How to use Map.Make after "hol.ml"?

[fblanqui]

Hello. Using ocaml.4.02.3 and campl5.6.17 I get the following problem:

#use "hol.ml";;
# module OrdInt = struct type t = int let compare = (-) end;;
Toplevel input:
# module OrdInt = struct type t = int let compare = (-) end;;
         ^^^^^^
Parse error: 'type' or 'rec' expected after 'module' (in [str_item])

Why can't I define modules anymore? How do I do to build maps on integers (Map.Make(OrdInt))?

[maggesi]

You can use

unset_jrh_lexer;;

to go back to normal OCaml syntax and

set_jrh_lexer;;

to reactivate CAML Light / HOL Light syntax.

[fblanqui]

Thanks!

[aqjune-aws]

Now we officially have a Help document for unset_jrh_lexer. :) https://github.com/jrh13/hol-light/blob/master/Help/unset_jrh_lexer.hlp