diff --git a/filter/base/filter_cache_fun.ml b/filter/base/filter_cache_fun.ml
index 85f5bbf4..d9c1166a 100644
--- a/filter/base/filter_cache_fun.ml
+++ b/filter/base/filter_cache_fun.ml
@@ -126,9 +126,7 @@ let string_of_op_shape shape =
          Buffer.add_char buf ']'
    in
    let string_of_arity i =
-      Buffer.add_char buf '<';
-      Buffer.add_string buf (string_of_int i);
-      Buffer.add_char buf '>'
+      Printf.bprintf buf "<%i>" i
    in
    let { sh_name = name;
          sh_kind = kind;
diff --git a/filter/base/filter_grammar.ml b/filter/base/filter_grammar.ml
index b5aa1b6a..3a9456e5 100644
--- a/filter/base/filter_grammar.ml
+++ b/filter/base/filter_grammar.ml
@@ -108,26 +108,6 @@ module Lexer = MakeLexer (Lm_channel.LexerInput) (Action);;
 (*
  * Boolean lexer is for parsing comments and quotations.
  *)
-(* unused
-module BoolCompare =
-struct
-   type t = bool
-
-   let compare b1 b2 =
-      if b1 then
-         if b2 then
-            0
-         else
-            1
-      else if b2 then
-         -1
-      else
-         0
-end
-
-module BoolSet = Lm_set.LmMake (BoolCompare);;
-*)
-
 module BoolAction =
 struct
    type action = bool
@@ -140,13 +120,7 @@ struct
       else
          0x5ffa1124
 
-   let compare a b =
-      if a = b then
-         0
-      else if a then
-         1
-      else
-         -1
+   let compare = Bool.compare
 
    let choose = max
 end;;
diff --git a/filter/base/filter_magic.ml b/filter/base/filter_magic.ml
index 9687abbb..c36ee3d8 100644
--- a/filter/base/filter_magic.ml
+++ b/filter/base/filter_magic.ml
@@ -39,7 +39,7 @@ open File_type_base
  ************************************************************************
  *
  * Current MD5 hash of the summary-related types (as computed by OMake):
- * FILTER_MD5: b2463ac8f553284fb92799f0d93fc130
+ * FILTER_MD5: 2cba8f8a16c795b59ef3e5d3b94bfb79
  *
  * The arguments for pack_version are:
  *    major version number, minor sub-version number, revision number
@@ -125,7 +125,6 @@ let term_versions = List.map (pack_version 1 0) [34;33;32;31;30;29;28;27;25;24]
  * Rev 27: changed the stging encoding of option_info
  * Rev 28: added "opaque" qualifier to the "define" statements
  *
- * Filter_summary has another HACK needed to read some rev 0-15 files.
  * Filter_summary has another HACK needed to read some rev 0-17 files.
  * Filter_summary has another HACK needed to read some rev 0-18 files.
  * Filter_summary has another HACK needed to read some rev 0-20 files.
diff --git a/filter/base/filter_ocaml.ml b/filter/base/filter_ocaml.ml
index b40f3a42..49507c9c 100644
--- a/filter/base/filter_ocaml.ml
+++ b/filter/base/filter_ocaml.ml
@@ -375,7 +375,12 @@ struct
       let loc = MLast.loc_of_expr e in
          mk_loc_term (Ploc.file_name loc) (Lm_num.num_of_int (Ploc.line_nb loc))
 
-   let value_names =
+   let type_name tdl =
+      match tdl.MLast.tdNam with
+         (<:vala< _, <:vala< name >> >>) -> mk_ident_term name
+       | _ -> invalid_arg "Filter_ocaml.type_name"
+
+   let value_name =
       let patt_tuple_op = mk_caml_op "tuple"
       and str_def_op = mk_caml_op "str_def" in
       let rec name_term = function
@@ -387,7 +392,7 @@ struct
             name_term p
        | (<:patt< ($list:lp$) >>) ->
             mk_simple_term patt_tuple_op [mk_olist_term name_term lp]
-       | _ -> invalid_arg "Filter_ocaml.value_names"
+       | _ -> invalid_arg "Filter_ocaml.value_name"
       in fun (p,e,_) -> mk_simple_term str_def_op [name_term p; loc_of_expr e]
 
    let mk_me_item me =
@@ -403,16 +408,16 @@ struct
 
    let mk_str_item =
       let str_external_op = mk_caml_op "str_ext"
-   (* and str_type_op = mk_caml_op "str_type" *)
+      and str_type_op = mk_caml_op "str_type"
       and str_fix_op = mk_caml_op "str_fix"
       and str_open_op = mk_caml_op "str_open"
       in fun vars -> function
          (<:str_item< external $s$ : $t$ = $list:ls$ $itemattrs:_$ >>) ->
             mk_simple_named_term str_external_op s (mk_type t :: List.map mk_simple_string ls)
-   (*  | (<:str_item< type $flag:b$ $list:tdl$ >>) ->
-            mk_simple_term str_type_op [mk_olist_term mk_tdl tdl] *)
+       | (<:str_item< type $flag:b$ $list:tdl$ >>) ->
+            mk_simple_term str_type_op [mk_bool b; mk_olist_term type_name tdl]
        | (<:str_item< value $flag:b$ $list:lpex$ >>) ->
-            mk_simple_term str_fix_op [mk_bool b; mk_olist_term value_names lpex]
+            mk_simple_term str_fix_op [mk_bool b; mk_olist_term value_name lpex]
        | (<:str_item< open $!:b$ $me$ $itemattrs:_$ >>) ->
             mk_simple_term str_open_op [mk_me_item me]
        | _ -> mk_stub_term str_opname
diff --git a/filter/base/filter_summary.ml b/filter/base/filter_summary.ml
index d2437110..3f294857 100644
--- a/filter/base/filter_summary.ml
+++ b/filter/base/filter_summary.ml
@@ -1016,15 +1016,9 @@ struct
 
    (*
     * Get the parameter list.
-    * XXX HACK: the try wrapper is only there for backwards compativility with
-    * old files (ASCII formats <= 1.0.15)
     *)
    let dest_rule_params convert t =
-      try
-         List.map (dest_rule_param convert) (dest_xlist t)
-      with
-         Failure _ ->
-            []
+      List.map (dest_rule_param convert) (dest_xlist t)
 
    (*
     * Get the list of resource updates
diff --git a/filter/filter/filter_convert.ml b/filter/filter/filter_convert.ml
index adf9ed04..603d4ef3 100644
--- a/filter/filter/filter_convert.ml
+++ b/filter/filter/filter_convert.ml
@@ -43,7 +43,7 @@ open Filter_cache
  * Show the file loading.
  *)
 let _ =
-   show_loading "Loading Convert%t"
+   show_loading "Loading Convert"
 
 (*
  * Include directories.
diff --git a/filter/filter/filter_prog.ml b/filter/filter/filter_prog.ml
index 6f8a9a94..82df6d85 100644
--- a/filter/filter/filter_prog.ml
+++ b/filter/filter/filter_prog.ml
@@ -59,7 +59,7 @@ open Proof_convert
  * Show the file loading.
  *)
 let _ =
-   show_loading "Loading Filter_prog%t"
+   show_loading "Loading Filter_prog"
 
 let debug_filter_prog =
    create_debug (**)
@@ -412,7 +412,7 @@ let expr_of_label loc = function
 
 (*
  * Print a message on loading, and catch errors.
- *    Lm_debug.show_loading "Loading name%t";
+ *    Lm_debug.show_loading "Loading name";
  *    try e with
  *       exn ->
  *          Refine_exn.stderr_exn name exn
@@ -422,7 +422,7 @@ let wrap_exn proc loc name e =
    <:expr<
       do {
          (* Print a message before the execution *)
-         Lm_debug.show_loading $str: "Loading " ^ name ^ "%t"$;
+         Lm_debug.show_loading $str: "Loading " ^ name$;
          (* Wrap the body to catch exceptions *)
          try $e$ with
          $lid: exn_id$ ->
@@ -1404,7 +1404,7 @@ let define_resource proc loc name res =
       [<:str_item< type $inp_name$ = $res.res_input$ >>;
        <:str_item< type $outp_name$ = $res.res_output$ >>;
        <:str_item< value $lid:get_resource_name name$ =
-         Mp_resource.create_resource $str:fqn$ (**)
+         Mp_resource.create_resource $str:fqn$
             ( $res.res_body$ : Mp_resource.resource_info $lid:inp_name$ '$intermediate$ $lid:outp_name$ ) >>]
 
 let rec is_list_expr = function
@@ -1531,8 +1531,10 @@ let define_magic_block proc loc { magic_name = name; magic_code = stmts } =
    let index = List.fold_left Filter_hash.hash_str_item 0 stmts in
       <:str_item< value $lid:name$ = $int:string_of_int index$ >> :: stmts
 
+(*
 let define_prefix loc s =
    [<:str_item< value _ = $lid:Infix.prefix_name s$ >>]
+*)
 
 (*
  * Prolog declares the refiner and dformer.
@@ -1559,7 +1561,7 @@ let implem_prolog proc loc name =
                                 $lid:global_num_var$) =
                             Ml_term.term_arrays_of_string $str:String.escaped marshalled_terms$>>]
    in
-      <:str_item< Lm_debug.show_loading $str: "Loading theory " ^ String.capitalize_ascii name ^ "%t"$ >>
+      <:str_item< Lm_debug.show_loading $str: "Loading theory " ^ String.capitalize_ascii name$ >>
       :: <:str_item< value $lid:local_refiner_id$ = $refiner_expr loc$ . null_refiner $str: name$ >>
       :: term_let
 
@@ -1580,7 +1582,7 @@ let implem_postlog proc loc =
                   Theory.thy_groupdesc = $str:proc.imp_groupdesc$;
                   Theory.thy_refiner = $lid:refiner_id$
                }>>;
-            <:str_item< Lm_debug.show_loading $str: ("Finished loading " ^ String.capitalize_ascii proc.imp_name ^ "%t") $ >>]
+            <:str_item< Lm_debug.show_loading $str:"Finished loading " ^ String.capitalize_ascii proc.imp_name$ >>]
 
 (*
  * Now extract the program.
@@ -1688,9 +1690,6 @@ let extract_str_item proc (item, loc) =
          if !debug_filter_prog then
             eprintf "Filter_prog.extract_str_item: magic block%t" eflush;
          define_magic_block proc loc block
-    | MLGramUpd (Infix s)
-    | MLGramUpd (Suffix s) ->
-         define_prefix loc s
     | DefineTerm (shapeclass, class_term, def)
       when is_shape_normal shapeclass ->
          define_term proc loc class_term def
@@ -1699,6 +1698,7 @@ let extract_str_item proc (item, loc) =
     | DeclareType _
     | DeclareTerm _
     | DeclareTypeRewrite _
+    | MLGramUpd _
     | Id _
     | Comment _
     | PRLGrammar _ ->
diff --git a/libmojave b/libmojave
index 6ee382ff..f5075673 160000
--- a/libmojave
+++ b/libmojave
@@ -1 +1 @@
-Subproject commit 6ee382ff50b36774593b0265787166612f97ee4a
+Subproject commit f5075673738b09ea2b1e9eb71bb91be78933bfcf
diff --git a/mllib/http_simple.ml b/mllib/http_simple.ml
index 0ddef9a7..0c7af86b 100644
--- a/mllib/http_simple.ml
+++ b/mllib/http_simple.ml
@@ -550,48 +550,49 @@ type uri_state =
 
 let colon = ':'
 
+let split_at i str =
+   let len = String.length str in
+   let si = succ i in
+      String.sub str 0 i, String.sub str si (len - si)
+
 let parse_uri s =
-   let len = String.length s in
-   let proto = Buffer.create 7 in
-   let host = Buffer.create 64 in
-   let port = Buffer.create 6 in
-   let file = Buffer.create 128 in
-   let rec search state j =
-      if j <> len then
-         let c = s.[j] in
-         let j' = succ j in
-            match state with
-               StateProto ->
-                  if c = colon then
-                     search StateHost j'
-                  else
-                     (Buffer.add_char proto c; search StateProto j')
-             | StateHost ->
-                  if c = colon then
-                     search StatePort j'
-                  else if c = '/' then
-                     search StateFile j'
-                  else
-                     (Buffer.add_char host c; search StateHost j')
-             | StatePort ->
-                  if c = '/' then
-                     search StateFile j'
-                  else
-                     (Buffer.add_char port c; search StatePort j')
-             | StateFile ->
-                  Buffer.add_char file c;
-                  search StateFile j'
+   let proto = ref "" in
+   let host = ref "" in
+   let port = ref "" in
+   let file = ref "" in
+   let rec search state s =
+      match state with
+         StateProto ->
+            (match String.index_opt s colon with
+                Some i -> let p, h = split_at i s in
+                             proto := p; search StateHost h
+              | None -> proto := s)
+       | StateHost ->
+            (match String.index_opt s colon with
+                Some i -> let h, p = split_at i s in
+                             host := h; search StatePort p
+              | None -> (match String.index_opt s '/' with
+                            Some i -> let h, f = split_at i s in
+                                         host := h; search StateFile f
+                          | None -> host := s))
+       | StatePort ->
+            (match String.index_opt s '/' with
+                Some i -> let p, f = split_at i s in
+                             port := p; search StateFile f
+              | None -> port := s)
+       | StateFile ->
+            file := s
    in
-   let _ = search StateProto 0 in
-      { uri_proto = Buffer.contents proto;
-        uri_host = Buffer.contents host;
+   let () = search StateProto s in
+      { uri_proto = !proto;
+        uri_host = !host;
         uri_port =
-           (let i = parse_int (Buffer.contents port) in
+           (let i = parse_int !port in
                if i = 0 then
                   None
                else
                   Some i);
-        uri_path = Buffer.contents file
+        uri_path = !file
       }
 
 let split_eq_val arg =
diff --git a/refiner/reflib/match_seq.ml b/refiner/reflib/match_seq.ml
index e0b9124c..73c1acb7 100644
--- a/refiner/reflib/match_seq.ml
+++ b/refiner/reflib/match_seq.ml
@@ -39,7 +39,7 @@ open Term
 open TermType
 open TermSubst
 
-let _ = show_loading "Loading Term_subst_ds%t"
+let () = show_loading "Loading Term_subst_ds"
 
 let cant_match_hyp = RefineError ("Match_seq.match_hyp", StringError "sequents do not match")
 let fail_match _ = raise cant_match_hyp
diff --git a/refiner/reflib/ml_term.ml b/refiner/reflib/ml_term.ml
index b04afd03..a6470810 100644
--- a/refiner/reflib/ml_term.ml
+++ b/refiner/reflib/ml_term.ml
@@ -37,7 +37,7 @@ open Term_io
 (*
  * Header.
  *)
-let magic = "MP-OCaml terms:"
+let magic = "MP-ML_terms:"
 let magic_len = String.length magic
 
 let check_magic s =
@@ -49,10 +49,10 @@ let check_magic s =
  *)
 let string_of_term_lists ts mts opnames nums =
    let terms =
-      List.map denormalize_term ts,
-      List.map denormalize_meta_term mts,
-      opnames,
-      nums
+      Lm_array_util.of_list_map denormalize_term ts,
+      Lm_array_util.of_list_map denormalize_meta_term mts,
+      Array.of_list opnames,
+      Array.of_list nums
    in
       magic ^ Marshal.to_string terms []
 
@@ -62,11 +62,11 @@ let string_of_term_lists ts mts opnames nums =
 let term_arrays_of_string s =
    check_magic s;
    let ts, mts, opnames, nums =
-      (Marshal.from_string s magic_len : Refiner_io.TermType.term list * Refiner_io.TermType.meta_term list * opname list * Lm_num.num list) in
-      Array.of_list (List.map normalize_term ts),
-      Array.of_list (List.map normalize_meta_term mts),
-      Array.of_list (List.map normalize_opname opnames),
-      Array.of_list nums
+      (Marshal.from_string s magic_len : Refiner_io.TermType.term array * Refiner_io.TermType.meta_term array * opname array * Lm_num.num array) in
+      Array.map normalize_term ts,
+      Array.map normalize_meta_term mts,
+      Array.map normalize_opname opnames,
+      nums
 
 (*
  * -*-
diff --git a/refiner/reflib/unify_mm.ml b/refiner/reflib/unify_mm.ml
index 6d46ea9e..831af05f 100644
--- a/refiner/reflib/unify_mm.ml
+++ b/refiner/reflib/unify_mm.ml
@@ -596,19 +596,19 @@ let rec terms2temp_multieq t0 t1 consts u var_hashtbl b_asslist0 b_asslist1 =
          let op_n0 =List.length tbvs_list0
          and op_n1 =List.length tbvs_list1 in
          if not (op_n0=op_n1) then raise(Clash(ClashTerms("terms2temp_multieq:7",t0,t1)));
-         let op_a0 = Array.of_list (List.map List.length tbvs_list0)
-         and op_a1 = Array.of_list (List.map List.length tbvs_list1) in
+         let op_a0 = Lm_array_util.of_list_map List.length tbvs_list0
+         and op_a1 = Lm_array_util.of_list_map List.length tbvs_list1 in
          if not (op_a0=op_a1) then raise(Clash(ClashTerms("terms2temp_multieq:8",t0,t1)));
          let fs = { opsymb = op0;
                     oparity_n = op_n0;
                     oparity_a = op_a0 ;
                     b_length = 2;
                     opbinding = (Array.init op_n0
-                                 (function i -> (Array.make op_a0.(i) [] )
+                                 (fun i -> (Array.make op_a0.(i) [] )
                                  )
                                 );
                     renamings = (Array.init op_n0
-                                 (function i -> (Array.make op_a0.(i) (V null_var) )
+                                 (fun i -> (Array.make op_a0.(i) (V null_var) )
                                  )
                                 );
                     timestamp = (-1)
diff --git a/refiner/rewrite/rewrite_compile_contractum.ml b/refiner/rewrite/rewrite_compile_contractum.ml
index dc205931..e45e27a4 100644
--- a/refiner/rewrite/rewrite_compile_contractum.ml
+++ b/refiner/rewrite/rewrite_compile_contractum.ml
@@ -55,8 +55,8 @@ open Rewrite_types
 (*
  * Show the file loading.
  *)
-let _ =
-   show_loading "Loading Rewrite_compile_contractum%t"
+let () =
+   show_loading "Loading Rewrite_compile_contractum"
 
 let debug_rewrite = load_debug "rewrite"
 
diff --git a/refiner/rewrite/rewrite_match_redex.ml b/refiner/rewrite/rewrite_match_redex.ml
index fac35441..e1dcdcd2 100644
--- a/refiner/rewrite/rewrite_match_redex.ml
+++ b/refiner/rewrite/rewrite_match_redex.ml
@@ -53,8 +53,8 @@ open Rewrite_types
 (*
  * Show the file loading.
  *)
-let _ =
-   show_loading "Loading Rewrite_match_redex%t"
+let () =
+   show_loading "Loading Rewrite_match_redex"
 
 let debug_rewrite = load_debug "rewrite"
 
diff --git a/refiner/rewrite/rewrite_util.ml b/refiner/rewrite/rewrite_util.ml
index c61aa072..40c52f33 100644
--- a/refiner/rewrite/rewrite_util.ml
+++ b/refiner/rewrite/rewrite_util.ml
@@ -41,8 +41,8 @@ open Refine_error_sig
 (*
  * Show the file loading.
  *)
-let _ =
-   show_loading "Loading Rewrite_util%t"
+let () =
+   show_loading "Loading Rewrite_util"
 
 let _debug_rewrite =
    create_debug (**)
diff --git a/refiner/term_gen/term_shape_gen.ml b/refiner/term_gen/term_shape_gen.ml
index 042d007a..7af8f652 100644
--- a/refiner/term_gen/term_shape_gen.ml
+++ b/refiner/term_gen/term_shape_gen.ml
@@ -198,22 +198,18 @@ struct
 
    let rec print_arity buf = function
       [i] ->
-         Buffer.add_string buf (string_of_int i)
+         Printf.bprintf buf "%i" i
     | i :: t ->
-         Buffer.add_string buf (string_of_int i);
-         Buffer.add_char buf ';';
+         Printf.bprintf buf "%i;" i;
          print_arity buf t
     | [] ->
          ()
 
    let string_of_shape { shape_opname = name; shape_params = params; shape_arities = arities } =
       let buf = Buffer.create 32 in
-         Buffer.add_string buf (string_of_opname name);
-         Buffer.add_char buf '[';
+         Printf.bprintf buf "%s[" (string_of_opname name);
          List.iter (print_param buf) params;
-         Buffer.add_string buf "]{";
-         print_arity buf arities;
-         Buffer.add_string buf "}";
+         Printf.bprintf buf "]{%a}" print_arity arities;
          Buffer.contents buf
 
    let string_of_opparam op =
@@ -236,9 +232,7 @@ struct
              [] ->
                 ()
            | _ ->
-                Buffer.add_char buf '{';
-                print_arity buf arities;
-                Buffer.add_char buf '}');
+                Printf.bprintf buf "{%a}" print_arity arities);
          Buffer.contents buf
 
    let print_shape out shape =
diff --git a/support/editor/mp_top.ml b/support/editor/mp_top.ml
index e560ebad..68dc9d7f 100644
--- a/support/editor/mp_top.ml
+++ b/support/editor/mp_top.ml
@@ -32,18 +32,18 @@
 open Lm_debug
 open Lm_printf
 
-let _ =
-   show_loading "Loading Mp_top%t"
+let () =
+   show_loading "Loading Mp_top"
 
 module Shell = Shell.Shell (Shell_mp.ShellP4)
 
-let _ =
-   show_loading "Loaded Shell%t"
+let () =
+   show_loading "Loaded Shell"
 
 module ShellBrowser = Shell_browser.ShellBrowser (Shell.Top)
 
-let _ =
-   show_loading "Starting main loop%t"
+let () =
+   show_loading "Starting main loop"
 
 (*
  * The first active shell will take everything.
diff --git a/support/shell/mptop.ml b/support/shell/mptop.ml
index 55808739..e20e4c49 100644
--- a/support/shell/mptop.ml
+++ b/support/shell/mptop.ml
@@ -187,8 +187,8 @@ and mk_expr top_expr =
             let names = string_list_of_longident li in
                VarProjExpr (names, v)
        | (<:expr< $lid: v$ . val >>) ->
-            let f = loc, VarExpr ("deref_" ^ v) in
-            let x = loc, UnitExpr () in
+            let f = loc, VarExpr ("deref_" ^ v)
+            and x = loc, UnitExpr () in
                ApplyExpr (f, x)
        | (<:expr< $e1$ $e2$ >>) as app_expr ->
             (match unapplist app_expr with
diff --git a/support/shell/shell.ml b/support/shell/shell.ml
index e407b958..236bd894 100644
--- a/support/shell/shell.ml
+++ b/support/shell/shell.ml
@@ -60,8 +60,8 @@ open Shell_current
 (*
  * Show that the file is loading.
  *)
-let _ =
-   show_loading "Loading Shell%t"
+let () =
+   show_loading "Loading Shell"
 
 (* unused
 let debug_shell  = load_debug "shell"
@@ -72,8 +72,8 @@ let debug_shell  = load_debug "shell"
  *)
 module Shell (ShellP4 : ShellP4Sig) =
 struct
-   let _ =
-      show_loading "Loading Shell module%t"
+   let () =
+      show_loading "Loading Shell module"
 
 (* unused
    type t = shell
diff --git a/support/shell/shell_browser.ml b/support/shell/shell_browser.ml
index 834a4765..7c3a0037 100644
--- a/support/shell/shell_browser.ml
+++ b/support/shell/shell_browser.ml
@@ -49,8 +49,8 @@ open Shell_sig
 open Shell_util
 open Shell_syscall_sig
 
-let _ =
-   show_loading "Loading Shell Browser%t"
+let () =
+   show_loading "Loading Shell Browser"
 
 let debug_http =
    create_debug (**)
diff --git a/support/shell/shell_core.ml b/support/shell/shell_core.ml
index 23b293d2..e2287aa8 100644
--- a/support/shell/shell_core.ml
+++ b/support/shell/shell_core.ml
@@ -46,12 +46,7 @@ open Shell_internal_sig
 
 let debug_refine = load_debug "refine"
 
-let debug_shell =
-   create_debug (**)
-      { debug_name = "shell";
-        debug_description = "Display shell operations";
-        debug_value = false
-      }
+let debug_shell = load_debug "shell"
 
 (*
  * We should skip the packages that do not have basic shell commands in them.
diff --git a/support/shell/shell_rule.ml b/support/shell/shell_rule.ml
index 207274aa..d93b0e90 100644
--- a/support/shell/shell_rule.ml
+++ b/support/shell/shell_rule.ml
@@ -54,8 +54,8 @@ open Filter_summary_type
 (*
  * Show that the file is loading.
  *)
-let _ =
-   show_loading "Loading Shell_rule%t"
+let () =
+   show_loading "Loading Shell_rule"
 
 let debug_shell =
    create_debug (**)
diff --git a/support/tactics/auto_tactic.ml b/support/tactics/auto_tactic.ml
index 9994953c..e94cd383 100644
--- a/support/tactics/auto_tactic.ml
+++ b/support/tactics/auto_tactic.ml
@@ -472,10 +472,6 @@ let debugT auto_tac =
 let map_progressT tac =
    { tac with auto_tac = progressT tac.auto_tac }
 
-let trivialP  tac = (tac.auto_type == AutoTrivial)
-let normalP   tac = (tac.auto_type == AutoNormal)
-let completeP tac = (tac.auto_type == AutoComplete)
-
 (*
  * Build an auto tactic from all of the tactics given.
  * A list of tactics to try is constructed.
@@ -513,46 +509,33 @@ let ifthenelseT tac1 tac2 tac3 =
       tryT tac thenT thenelseT
 
 let extract tactics =
-   let tactics =
-      if !debug_auto then List.map debugT tactics
-      else List.map map_progressT tactics
+   let mapT =
+      if !debug_auto then debugT else map_progressT
    in
-   let trivial = sort_nodes (List.filter trivialP tactics) in
-   let normal = sort_nodes (List.filter normalP tactics) in
-   let complete = sort_nodes (List.filter completeP tactics) in
+   let trivial, normal, complete =
+      List.fold_left (fun (t, n, c) tac ->
+            let tac = mapT tac in
+               match tac.auto_type with
+                  AutoTrivial -> tac::t, n, c
+                | AutoNormal -> t, tac::n, c
+                | AutoComplete -> t, n, tac::c
+      ) ([],[],[]) tactics in
+	 let trivial = sort_nodes trivial
+   and normal = sort_nodes normal
+   and complete = sort_nodes complete in
    if !debug_auto then begin
       let names tacs = String.concat "; " (List.map (fun t -> t.auto_name) tacs) in
       eprintf "Auto tactics:\n\tTrivial: %s\n\tNormal: %s\n\tComplete: %s%t"
          (names trivial) (names normal) (names complete) eflush;
    end;
-   let make_progress_first reset next tacloop =
-      let rec prog_first tacs goals =
-         match tacs with
-            [] ->
-               next goals
-          | tac :: tacs ->
-               ifthenelseT tac.auto_tac (make_progressT goals prog_reset tacloop) (prog_first tacs goals)
-      and prog_reset goals = prog_first reset goals
-      in
-         prog_first
-   in
-   let next_idT _ = idT in
-   let next_failT _ = failT in
-   let trivT = make_progress_first trivial next_idT idT trivial ShapeMTable.empty in
-   let normal_tacs = trivial @ normal in
-   let all_tacs = trivial @ normal @ complete in
-   let try_complete goals = tryT (make_progress_first all_tacs next_failT failT complete goals) in
-   let autoT = make_progress_first normal_tacs try_complete idT normal_tacs ShapeMTable.empty in
-   let strongAutoT = make_progress_first all_tacs next_idT idT all_tacs ShapeMTable.empty in
-   let caT = make_progress_first all_tacs next_failT failT all_tacs ShapeMTable.empty in
-      (trivT, autoT, strongAutoT, caT)
+   trivial, normal, complete
 
 let improve_resource data info = info::data
 
 (*
  * Resource.
  *)
-let resource (auto_info, tactic * tactic * tactic * tactic) auto =
+let resource (auto_info, auto_info list * auto_info list * auto_info list) auto =
    Functional {
       fp_empty = [];
       fp_add = improve_resource;
@@ -585,17 +568,40 @@ let rec check_progress goal = function
 (*
  * Actual tactics.
  *)
+let make_progress_first reset next tacloop =
+   let rec prog_first tacs goals =
+      match tacs with
+         [] ->
+            next goals
+       | tac :: tacs ->
+            ifthenelseT tac.auto_tac (make_progressT goals prog_reset tacloop) (prog_first tacs goals)
+   and prog_reset goals = prog_first reset goals
+   in
+      prog_first
+
+let next_idT _ = idT
+let next_failT _ = failT
+
 let trivialT =
-   funT (fun p -> let trivT, _, _, _ = get_resource_arg p get_auto_resource in trivT)
+   funT (fun p -> let trivial, _, _ = get_resource_arg p get_auto_resource in
+                     make_progress_first trivial next_idT idT trivial ShapeMTable.empty)
 
 let autoT =
-   funT (fun p -> let _, autoT, _, _ = get_resource_arg p get_auto_resource in autoT)
+   funT (fun p -> let trivial, normal, complete = get_resource_arg p get_auto_resource in
+                  let normal_tacs = trivial @ normal in
+                  let all_tacs = normal_tacs @ complete in
+                  let try_complete goals = tryT (make_progress_first all_tacs next_failT failT complete goals) in
+                     make_progress_first normal_tacs try_complete idT normal_tacs ShapeMTable.empty)
 
 let strongAutoT =
-   funT (fun p -> let _, _, sAutoT, _ = get_resource_arg p get_auto_resource in sAutoT)
+   funT (fun p -> let trivial, normal, complete = get_resource_arg p get_auto_resource in
+                  let all_tacs = trivial @ normal @ complete in
+                     make_progress_first all_tacs next_idT idT all_tacs ShapeMTable.empty)
 
 let completeAutoT =
-   funT (fun p -> let _, _, _, tca = get_resource_arg p get_auto_resource in tca)
+   funT (fun p -> let trivial, normal, complete = get_resource_arg p get_auto_resource in
+                  let all_tacs = trivial @ normal @ complete in
+                     make_progress_first all_tacs next_failT failT all_tacs ShapeMTable.empty)
 
 let tcaT = tryT completeAutoT
 
diff --git a/support/tactics/auto_tactic.mli b/support/tactics/auto_tactic.mli
index 434707ed..ce525e52 100644
--- a/support/tactics/auto_tactic.mli
+++ b/support/tactics/auto_tactic.mli
@@ -93,7 +93,7 @@ and auto_type =
  | AutoNormal
  | AutoComplete
 
-resource (auto_info, tactic * tactic * tactic * tactic) auto
+resource (auto_info, auto_info list * auto_info list * auto_info list) auto
 
 (*
  * Operations on precedences.
diff --git a/support/tactics/top_tacticals.ml b/support/tactics/top_tacticals.ml
index da2b92e9..cf3cd6b7 100644
--- a/support/tactics/top_tacticals.ml
+++ b/support/tactics/top_tacticals.ml
@@ -187,7 +187,7 @@ let prefix_andalsoT = Tacticals.prefix_andalsoT
 let prefix_orthenT = Tacticals.prefix_orthenT
 let firstT = Tacticals.firstT
 let prefix_thenLT = Tacticals.prefix_thenLT
-let prefix_thenFLT = Tacticals.prefix_thenFLT
+(* let prefix_thenFLT = Tacticals.prefix_thenFLT *)
 let seqT = Tacticals.seqT
 let seqOnSameConclT = Tacticals.seqOnSameConclT
 let prefix_thenT = Tacticals.prefix_thenT
diff --git a/tactics/proof/conversionals_boot.ml b/tactics/proof/conversionals_boot.ml
index d35be310..3f31782e 100644
--- a/tactics/proof/conversionals_boot.ml
+++ b/tactics/proof/conversionals_boot.ml
@@ -51,8 +51,8 @@ open Tacticals_boot
 (*
  * Debug statement.
  *)
-let _ =
-   show_loading "Loading Conversionals_boot%t"
+let () =
+   show_loading "Loading Conversionals_boot"
 
 (* unused
 let debug_conv =
@@ -106,7 +106,7 @@ struct
    let failWithC s =
       funC (fun _ -> raise (RefineError ("failWithC", StringError s)))
 
-   let failC  =  failWithC "Fail"
+   let failC = failWithC "Fail"
 
    (*
     * Trial.
@@ -156,52 +156,52 @@ struct
    (*
     * Apply to leftmost-innermost term.
     *)
-   let rec lowerC rw =
-      let lowerCE e =
-         prefix_orelseC (someSubC (lowerC rw)) rw
+   let lowerC rw =
+      let rec lowerCE e =
+         prefix_orelseC (someSubC (funC lowerCE)) rw
       in
          funC lowerCE
 
    (*
     * Apply to all terms possible from innermost to outermost.
     *)
-   let rec sweepUpC rw =
-      let sweepUpCE e =
-         prefix_thenC (allSubC (sweepUpC rw)) (tryC rw)
+   let sweepUpC rw =
+      let rec sweepUpCE e =
+         prefix_thenC (allSubC (funC sweepUpCE)) (tryC rw)
       in
          funC sweepUpCE
 
-   let rec sweepDnC rw =
-      let sweepDnCE e =
-         prefix_thenC (tryC rw) (allSubC (sweepDnC rw))
+   let sweepDnC rw =
+      let rec sweepDnCE e =
+         prefix_thenC (tryC rw) (allSubC (funC sweepDnCE))
       in
          funC sweepDnCE
 
    (*
     * These are the same but don't allow failure.
     *)
-   let rec sweepUpFailC rw =
-      let sweepUpCE e =
-         prefix_thenC (allSubC (sweepUpFailC rw)) rw
+   let sweepUpFailC rw =
+      let rec sweepUpCE e =
+         prefix_thenC (allSubC (funC sweepUpCE)) rw
       in
          funC sweepUpCE
 
-   let rec sweepDnFailC rw =
-      let sweepDnCE e =
-         prefix_thenC rw (allSubC (sweepDnFailC rw))
+   let sweepDnFailC rw =
+      let rec sweepDnCE e =
+         prefix_thenC rw (allSubC (funC sweepDnCE))
       in
          funC sweepDnCE
 
    (*
     * Search for the term, then apply conversion.
     *)
-   let rec findThenC test rw =
-      let findThenCE e =
+   let findThenC test rw =
+      let rec findThenCE e =
          let t = env_term e in
             if test t then
                rw
             else
-               allSubC (findThenC test rw)
+               allSubC (funC findThenCE)
       in
          funC findThenCE
 
@@ -243,22 +243,22 @@ struct
     * Repeat the conversion until fails.
     *)
    let untilFailC conv =
-      let rec aux env =
-         (tryC (prefix_thenC conv (funC aux)))
+      let rec aux _ =
+         tryC (prefix_thenC conv (funC aux))
       in
          funC aux
 
-   let rec repeatForC i conv =
+   let repeatForC i conv =
       if i < 0 then
          raise (Invalid_argument "repeatForC: the argument should be not negative")
       else
-         let repeatForCE env =
+         let rec repeatForCE i =
             if i = 0 then
                idC
             else
-               prefix_thenC conv (repeatForC (i - 1) conv)
+               prefix_thenC conv (funC (fun _ -> repeatForCE (i - 1)))
          in
-            funC repeatForCE
+            repeatForCE i
 
    let rwc conv assum clause =
       Rewrite.rw conv assum (TermAddr.make_address [ClauseAddr clause])
diff --git a/tactics/proof/proof_boot.ml b/tactics/proof/proof_boot.ml
index 89a6e97e..6595d73b 100644
--- a/tactics/proof/proof_boot.ml
+++ b/tactics/proof/proof_boot.ml
@@ -1262,9 +1262,9 @@ struct
          collect_opname (fun x -> x) (dest_opname opname)
 
    let describe_args (opname, ints, addrs, params) =
-      let ints = Array.of_list (List.map (fun addr -> IntArg addr) ints) in
-      let addrs = Array.of_list (List.map (fun addr -> AddrArg addr) addrs) in
-      let params = Array.of_list (List.map (fun t -> TermArg t) params) in
+      let ints = Lm_array_util.of_list_map (fun addr -> IntArg addr) ints in
+      let addrs = Lm_array_util.of_list_map (fun addr -> AddrArg addr) addrs in
+      let params = Lm_array_util.of_list_map (fun t -> TermArg t) params in
       let name = [|StringArg (string_of_opname opname)|] in
          Array.concat [name; ints; addrs; params]
 
diff --git a/tactics/proof/tacticals_boot.ml b/tactics/proof/tacticals_boot.ml
index be83d86b..313c3214 100644
--- a/tactics/proof/tacticals_boot.ml
+++ b/tactics/proof/tacticals_boot.ml
@@ -42,13 +42,13 @@ open Refiner.Refiner.TermType
 
 open Tactic_boot
 open Sequent_boot
-open Tactic_boot_sig
+(* open Tactic_boot_sig *)
 
 (*
  * Debug statement.
  *)
-let _ =
-   show_loading "Loading Tacticals_boot%t"
+let () =
+   show_loading "Loading Tacticals_boot"
 
 (* unused
 let debug_subgoals =
@@ -59,12 +59,7 @@ let debug_subgoals =
       }
 *)
 
-let debug_profile_tactics =
-   create_debug (**)
-      { debug_name = "profile_tactics";
-        debug_description = "Collect and report profiling information for top-level tactics (not theads-safe)";
-        debug_value = false
-      }
+(* let debug_profile_tactics = load_debug "profile_tactics" *)
 
 module Tacticals =
 struct
@@ -461,10 +456,10 @@ struct
          prefix_thenFLT tac1 (aux tacs)
 
    let prefix_thenMLT =
-      thenLLT (function l -> isEmptyOrMainLabel l)
+      thenLLT isEmptyOrMainLabel
 
    let prefix_thenALT =
-      thenLLT (function l -> isAuxLabel l)
+      thenLLT isAuxLabel
 
    (************************************************************************
     * LABEL PROGRESS                                                       *
@@ -829,6 +824,7 @@ struct
    let get_alt_arg arg =
       match Sequent.get_bool_arg arg "alt" with Some v -> v | None -> false
 
+(* disabled
    let table = Hashtbl.create 19
 
    let profileWrapT args tac =
@@ -886,9 +882,10 @@ struct
                         raise exn
                end else
                   TacticInternal.wrapT args tac p
+*)
 
-   let wrapT =
-      if !debug_profile_tactics then profileWrapT else TacticInternal.wrapT
+   let wrapT = (* XXX: this is not working due to debug argument setting is too late *)
+      (* if !debug_profile_tactics then profileWrapT else *) TacticInternal.wrapT
 
 end
 
diff --git a/theories b/theories
index 8e317001..eb3dcf3d 160000
--- a/theories
+++ b/theories
@@ -1 +1 @@
-Subproject commit 8e317001bf62ebceb59d45809c4b8b76294917f6
+Subproject commit eb3dcf3d83a8ac407f92516991078eb5f5a15093
diff --git a/util/ocamldep.mll b/util/ocamldep.mll
index 85029dd2..c7d68817 100644
--- a/util/ocamldep.mll
+++ b/util/ocamldep.mll
@@ -28,14 +28,9 @@
  * @end[license]
  *)
 {
-module StringCompare =
-struct
-   type t = string
-   let compare = Stdlib.compare
-end;;
 
-module StringSet = Set.Make (StringCompare);;
-module StringTable = Map.Make (StringCompare);;
+module StringSet = Set.Make (String)
+module StringTable = Map.Make (String)
 
 type summary =
    { summ_basename        : string;
@@ -536,7 +531,7 @@ let summ_reflect summ =
    (* The theories will be extending Basic_tactics *)
    let free_structures =
       if is_impl then
-         List.fold_left (fun set name -> StringSet.add name set) StringSet.empty reflect_modules
+         StringSet.of_list reflect_modules
       else
          StringSet.empty
    in
diff --git a/util/pa_macro.ml b/util/pa_macro.ml
index 5413fe7c..08c4b1c5 100644
--- a/util/pa_macro.ml
+++ b/util/pa_macro.ml
@@ -235,6 +235,8 @@ value substp mloc env =
     | <:expr< $uid:x$ >> ->
         try List.assoc x env with
         [ Not_found -> <:patt< $uid:x$ >> ]
+    | <:expr:< $longid:li$ >> ->
+      <:patt< $longid:li$ >>
     | <:expr< $int:x$ >> -> <:patt< $int:x$ >>
     | <:expr< $str:s$ >> -> <:patt< $str:s$ >>
     | <:expr< ($list:x$) >> -> <:patt< ($list:List.map loop x$) >>