diff --git a/compiler/bootstrap/translation/caml_lexProgScript.sml b/compiler/bootstrap/translation/caml_lexProgScript.sml
index e0075761b8..c51607fbc1 100644
--- a/compiler/bootstrap/translation/caml_lexProgScript.sml
+++ b/compiler/bootstrap/translation/caml_lexProgScript.sml
@@ -11,6 +11,7 @@ open preamble caml_lexTheory;
 open parserProgTheory ml_translatorLib ml_translatorTheory;
 
 val _ = translation_extends "parserProg";
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "caml_lexProg");
 
 (* -------------------------------------------------------------------------
  * Translator setup
@@ -157,6 +158,6 @@ val r = translate scan_float_or_int_def;
 val r = translate (caml_lexTheory.next_sym_def |> REWRITE_RULE [GSYM sub_check_def]);
 
 val r = translate caml_lexTheory.lexer_fun_def;
-
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 
 val () = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/reg_allocProgScript.sml b/compiler/bootstrap/translation/reg_allocProgScript.sml
index 65f265ecad..8edae2d67f 100644
--- a/compiler/bootstrap/translation/reg_allocProgScript.sml
+++ b/compiler/bootstrap/translation/reg_allocProgScript.sml
@@ -20,6 +20,8 @@ open basisProgTheory
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
 val _ = translation_extends "pancake_parseProg";
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "reg_allocProg");
+
 val _ = ml_translatorLib.use_sub_check true;
 (*
 val _ = translation_extends "basisProg";
@@ -451,4 +453,5 @@ val _ = disable_astPP()
 
 *)
 
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = (ml_translatorLib.clean_on_exit := true);
diff --git a/translator/alist_tree2Lib.sig b/translator/alist_tree2Lib.sig
new file mode 100644
index 0000000000..d8d0f28506
--- /dev/null
+++ b/translator/alist_tree2Lib.sig
@@ -0,0 +1,52 @@
+(* Code to recall that some partial functions (of type 'a -> 'b option)
+can be represented as sorted alists, and derive a fast conversion on
+applications of those functions. *)
+
+signature alist_tree2Lib = sig
+
+include Abbrev
+
+(* Syntax *)
+val alookup_tm : term;
+val option_choice_tm : term;
+val repr_tm : term;
+
+(* The repr set type *)
+type 'a alist_reprs
+
+(*
+   Representations of partial functions using sorted trees.
+   Requires a relation R and a theorem that shows
+   it is irreflexive and transitive. The destructor maps terms
+   of the domain type to some type that can be sorted in ML.
+   The conversion must prove R x y for any x, y where x is
+   sorted before y by the destructor and comparison.
+*)
+val mk_alist_reprs : thm -> conv -> (term -> 'a)
+    -> (('a * 'a) -> order) -> 'a alist_reprs
+
+(*
+   The representation set contains representations of various
+   partial functions, initially none.
+*)
+val peek_functions_in_rs : 'a alist_reprs -> term list
+
+(*
+   Adds a function's representation.
+
+   Requires a theorem f = rhs with a valid rhs.
+   A valid rhs is:
+     - ALOOKUP xs
+     - a function g in the repr set.
+     - option_choice_f of two valid rhs values
+*)
+val add_alist_repr : 'a alist_reprs -> thm -> unit
+
+(*
+   Converts f x to a concrete value (SOME y/NONE)
+   for functions f in the repr set.
+*)
+val reprs_conv : 'a alist_reprs -> conv
+
+end
+
diff --git a/translator/alist_tree2Lib.sml b/translator/alist_tree2Lib.sml
new file mode 100644
index 0000000000..180e0b68a6
--- /dev/null
+++ b/translator/alist_tree2Lib.sml
@@ -0,0 +1,398 @@
+(*
+  Code to recall that some partial functions (of type 'a -> 'b option)
+  can be represented as sorted alists, and derive a fast conversion on
+  applications of those functions.
+*)
+structure alist_tree2Lib :> alist_tree2Lib =
+struct
+
+open HolKernel Parse boolLib simpLib bossLib
+
+open alist_treeTheory comparisonTheory
+
+(* Copied from Drule.sml faster than ISPECL for subtituting big terms*)
+local
+   fun strip [] _ = []     (* Returns a list of (pat,ob) pairs. *)
+     | strip (tm :: tml) M =
+         let
+            val (Bvar, Body) = dest_forall M
+         in
+            (type_of Bvar, type_of tm)::strip tml Body
+         end
+   fun merge [] theta = theta
+     | merge ((x as {redex, residue})::rst) theta =
+       case subst_assoc (equal redex) theta of
+          NONE      => x :: merge rst theta
+        | SOME rdue => if residue = rdue then merge rst theta
+                       else raise ERR "ISPECL" ""
+   fun err s = raise ERR "ISPECL" s
+in
+   fun ISPECL [] = I
+     | ISPECL [tm] = ISPEC tm
+     | ISPECL tms =
+        fn th =>
+           let
+              val pairs =
+                 strip tms (concl th)
+                 handle HOL_ERR _ => err "list of terms too long for theorem"
+              val inst =
+                 rev_itlist
+                    (fn (pat, ob) => fn ty_theta =>
+                        let
+                           val theta = Type.match_type pat ob
+                        in
+                           merge theta ty_theta
+                        end) pairs []
+                 handle HOL_ERR _ => err "can't type-instantiate input theorem"
+              val genvars = List.map (genvar o type_of) tms
+              val ss = ListPair.map (op |->) (genvars,tms)
+           in
+              INST_TYPE inst th
+              |> SPECL genvars
+              |> INST ss
+              handle HOL_ERR _ => err "type variable free in assumptions"
+           end
+end
+
+(* Syntax *)
+
+val alookup_tm = prim_mk_const {Name = "ALOOKUP", Thy = "alist"}
+
+fun mkc nm = prim_mk_const {Name = nm, Thy = "alist_tree"}
+
+val count_append_tm = mkc "count_append"
+val is_insert_tm = mkc "is_insert"
+val option_choice_tm = mkc "option_choice_f"
+val is_lookup_tm = mkc "is_lookup"
+val repr_tm = mkc "sorted_alist_repr"
+
+(* trivia *)
+val err = mk_HOL_ERR "alist_treeLib"
+
+(* the repr set object *)
+datatype 'a alist_reprs = AList_Reprs of {R_thm: thm, conv: conv,
+    dest: term -> 'a, cmp: ('a * 'a) -> order,
+    dict: (term, thm) Redblackmap.dict ref}
+
+fun mk_alist_reprs R_thm conv dest cmp
+    = AList_Reprs {R_thm = R_thm, conv = conv, cmp = cmp,
+        dest = dest, dict = ref (Redblackmap.mkDict Term.compare)}
+
+fun peek_functions_in_rs (AList_Reprs inn_rs)
+    = Redblackmap.listItems (! (#dict inn_rs)) |> map fst
+
+fun peek_repr (AList_Reprs inn_rs) tm = Redblackmap.peek (! (#dict inn_rs), tm)
+
+(* constructing is_insert thms *)
+
+fun find_key_rec is_last [] = raise Empty
+  | find_key_rec is_last (t :: ts) = if listSyntax.is_nil t
+  then find_key_rec is_last ts
+  else let
+    val (f, xs) = strip_comb t
+    val do_rev = if is_last then rev else I
+  in if same_const f count_append_tm
+    then find_key_rec is_last (do_rev (tl xs) @ ts)
+    else hd (do_rev (fst (listSyntax.dest_list t))) end
+
+fun hd_key t = find_key_rec false [t] |> pairSyntax.dest_pair |> fst
+fun last_key t = find_key_rec true [t] |> pairSyntax.dest_pair |> fst
+
+fun mk_singleton x = listSyntax.mk_list ([x], type_of x)
+
+val simp_count_append = SIMP_CONV bool_ss [count_append_HD_LAST, pairTheory.FST]
+
+fun assume_prems thm = if not (is_imp (concl thm)) then thm
+  else let
+    val thm = CONV_RULE (RATOR_CONV simp_count_append) thm
+    val l_asm = fst (dest_imp (concl thm))
+    val prem = if l_asm ~~ T then TRUTH else ASSUME l_asm
+  in
+    assume_prems (MP thm prem)
+  end
+
+fun do_inst_mp insts mp_thm arg_thm = let
+    val (prem, _) = dest_imp (concl mp_thm)
+    fun rerr e s = let
+        val m = s ^ ": " ^ message_of e
+      in print ("error in do_inst_mp: " ^ m ^ "\n");
+        print_thm mp_thm; print "\n"; print_thm arg_thm; print "\n";
+        raise (err "do_inst_mp" m) end
+    val (more_insts, ty_insts) = match_term prem (concl arg_thm)
+      handle HOL_ERR e => rerr e "match_term"
+    val ty_i_thm = INST_TYPE ty_insts mp_thm
+    val ithm = INST (more_insts @ insts) ty_i_thm
+      handle HOL_ERR e => rerr e "INST"
+  in MP ithm arg_thm handle HOL_ERR e => rerr e "MP" end
+
+fun build_insert (dest : term -> 'a) cmp R k x =
+  let
+    val dest_k = dest k
+    fun chk thm = if same_const is_insert_tm (fst (strip_comb (concl thm)))
+      then thm
+      else (print "Not an insert_tm:\n"; print_thm thm; print "\n";
+        raise (err "build_insert" "check"))
+    val pp = chk o assume_prems
+    fun build t = if listSyntax.is_nil t
+      then pp (ISPECL [R, k, x] is_insert_to_empty)
+      else if listSyntax.is_cons t then let
+        val (xs, _) = listSyntax.dest_list t
+        val _ = length xs = 1 orelse raise (err "build_insert" "malformed")
+        val v = hd xs
+      in case cmp (dest_k, dest (fst (pairSyntax.dest_pair v))) of
+          EQUAL => pp (ISPECL [R, k, x, v] is_insert_overwrite)
+        | GREATER => pp (ISPECL [R, k, x, t] is_insert_far_right)
+        | LESS => pp (ISPECL [R, k, x, t] is_insert_far_left)
+      end else let
+        val (f, xs) = strip_comb t
+        val _ = same_const count_append_tm f
+           orelse raise (err "build_insert" "unknown")
+        val (n, l, r) = case xs of [n, l, r] => (n, l, r)
+           | _ => raise (err "build_insert" "num args")
+        fun vsub nm v = [mk_var (nm, type_of v) |-> v]
+      in if not (cmp (dest_k, dest (hd_key r)) = LESS)
+        then do_inst_mp (vsub "l" l) (SPEC n is_insert_r) (build r)
+        else if cmp (dest_k, dest (last_key l)) = GREATER
+        then ISPECL [R, n, k, x] is_insert_centre
+            |> INST (vsub "l" l @ vsub "r" r) |> pp
+        else do_inst_mp (vsub "r" r) (SPEC n is_insert_l) (build l)
+      end
+  in build end
+
+fun prove_assum_by_conv conv thm = let
+    val (x,y) = dest_imp (concl thm)
+    val thm = CONV_RULE ((RATOR_CONV o RAND_CONV) conv) thm
+  in MP thm TRUTH handle HOL_ERR e =>
+    (print "Failed to prove assum by conv:\n";
+      print_term x;
+      print "\n  -- reduced to:\n";
+      print_term (fst (dest_imp (concl thm)));
+      raise HOL_ERR e)
+  end
+
+(* balancing count_append trees *)
+fun get_depth tm = let
+    val (f, xs) = strip_comb tm
+  in if same_const f count_append_tm
+    then numSyntax.int_of_term (hd xs)
+    else if listSyntax.is_cons tm then 1
+    else raise (err "get_depth" "unknown")
+  end
+
+fun balance iter bias tm = if iter > 1000 then
+    (print "error: looping balance\n"; print_term tm;
+        raise (err "balance" "looping"))
+  else let
+    val (f, xs) = strip_comb tm
+    val _ = same_const f count_append_tm orelse raise UNCHANGED
+    val _ = is_arb (hd xs) orelse bias <> "N" orelse raise UNCHANGED
+    val step_conv = (RAND_CONV (balance 0 "N"))
+        THENC (RATOR_CONV (RAND_CONV (balance 0 "N")))
+    val thm = QCONV step_conv tm
+    val tm = rhs (concl thm)
+    val l_sz = get_depth (rand (rator tm))
+    val r_sz = get_depth (rand tm)
+    val reb = if l_sz > (r_sz + 1) orelse (bias = "R" andalso l_sz > r_sz)
+        then "R"
+        else if r_sz > (l_sz + 1) orelse (bias = "L" andalso r_sz > l_sz)
+        then "L" else "N"
+    val conv1 = if reb = "R" then RATOR_CONV (RAND_CONV (balance 0 "L"))
+        else if reb = "L" then RAND_CONV (balance 0 "R") else ALL_CONV
+    val conv2 = if reb = "R" then REWR_CONV balance_r
+        else if reb = "L" then REWR_CONV balance_l else ALL_CONV
+    val thm = CONV_RULE (QCONV (RHS_CONV (conv1 THENC conv2 THENC step_conv))) thm
+    val tm = rhs (concl thm)
+    val l_sz = get_depth (rand (rator tm))
+    val r_sz = get_depth (rand tm)
+    val sz = numSyntax.term_of_int (1 + Int.max (l_sz, r_sz))
+    val set = REWR_CONV (set_count |> SPEC sz)
+    val final = if Int.abs (l_sz - r_sz) < 2 then set else balance (iter + 1) "N"
+  in CONV_RULE (RHS_CONV final) thm end
+
+fun prove_insert R conv dest cmp k x al = let
+    val thm = build_insert dest cmp R k x al
+    fun prove thm = if not (is_imp (concl thm)) then thm
+      else prove (prove_assum_by_conv conv thm)
+  in thm |> DISCH_ALL |> prove |> CONV_RULE (RAND_CONV (balance 0 "N")) end
+
+(* making repr theorems *)
+
+fun mk_insert_repr (AList_Reprs rs) prev_repr k_x = let
+    val (k, x) = pairSyntax.dest_pair k_x
+    val (R, al) = case strip_comb (concl prev_repr)
+      of (_, [R, al, _]) => (R, al)
+        | _ => raise (err "mk_insert_repr" "unexpected")
+    val insert = prove_insert R (#conv rs) (#dest rs) (#cmp rs) k x al
+  in MATCH_MP repr_insert (CONJ prev_repr insert) end
+
+fun dest_alookup_single tm = let
+    val (f, xs) = strip_comb tm
+  in if not (length xs = 1 andalso same_const f alookup_tm)
+    then NONE
+    else if listSyntax.is_nil (hd xs) then SOME NONE
+    else case total listSyntax.dest_cons (hd xs) of
+        SOME (y, ys) => if listSyntax.is_nil ys then SOME (SOME y) else NONE
+      | NONE => NONE
+  end
+
+fun mk_repr_step rs tm = let
+    val (AList_Reprs inn_rs) = rs
+    val (f, xs) = strip_comb tm
+    val is_short =
+        not (option_eq (option_eq aconv) (dest_alookup_single tm) NONE)
+    val is_merge = same_const option_choice_tm f
+    val is_repr_merge = is_merge andalso (case peek_repr rs (hd xs) of
+        SOME _ => true | NONE => false)
+    val (is_insert, insert_tm) = if not is_merge then (false, T)
+        else case dest_alookup_single (hd xs) of
+            SOME (SOME t) => (true, t) | _ => (false, T)
+  in if is_short
+    then MATCH_MP (ISPEC (hd xs) alist_repr_refl) (#R_thm inn_rs)
+        |> prove_assum_by_conv (SIMP_CONV list_ss [sortingTheory.SORTED_DEF])
+    else if is_insert
+    then mk_insert_repr rs (mk_repr rs (rand tm)) insert_tm
+    else if is_repr_merge
+    then let
+        val l_repr_thm = mk_repr rs (hd xs)
+        val l_repr_al = rand (rator (concl l_repr_thm))
+        val look = mk_icomb (alookup_tm, l_repr_al)
+        val half_repr = list_mk_icomb (option_choice_tm, [look, List.last xs])
+        val next_repr = mk_repr rs half_repr
+      in MATCH_MP alist_repr_choice_trans_left (CONJ l_repr_thm next_repr) end
+    else CHANGED_CONV (SIMP_CONV bool_ss [alookup_to_option_choice,
+                option_choice_f_assoc, alookup_empty_option_choice_f,
+                count_append_def, alookup_append_option_choice_f,
+                empty_is_ALOOKUP]) tm
+        handle HOL_ERR _ => raise err "mk_repr_step"
+            ("no progress from SIMP_CONV: " ^ Parse.term_to_string tm)
+  end
+and mk_repr_known_step rs tm =
+  case peek_repr rs tm of
+    SOME thm => thm
+  | NONE => mk_repr_step rs tm
+and mk_repr rs tm = let
+    val thm = mk_repr_known_step rs tm
+  in if is_eq (concl thm)
+    then mk_repr rs (rhs (concl thm))
+      |> CONV_RULE (RAND_CONV (REWR_CONV (SYM thm)))
+    else thm
+  end
+
+fun add_alist_repr rs thm = let
+    val AList_Reprs inn_rs = rs
+    val (f, rhs) = dest_eq (concl thm)
+    val repr_thm = case peek_repr rs rhs of
+        SOME rhs_thm => if is_eq (concl rhs_thm)
+          then TRANS thm rhs_thm
+          else thm
+      | NONE => (mk_repr rs rhs
+        |> CONV_RULE (RAND_CONV (REWR_CONV (SYM thm))))
+  in
+    #dict inn_rs := Redblackmap.insert (! (#dict inn_rs), f, repr_thm)
+  end
+
+fun timeit msg f v = let
+    val start = Portable.timestamp ()
+    val r = f v
+    val time = Time.-(Portable.timestamp (), start)
+  in print ("Time to " ^ msg ^ ": " ^ Portable.time_to_string time ^ "\n");
+    r end
+
+(* testing *)
+
+fun test_rs () = let
+    val thm1 = DB.fetch "comparison" "good_cmp_Less_irrefl_trans"
+    val thm2 = DB.fetch "comparison" "num_cmp_good"
+    val R_thm = MATCH_MP thm1 thm2
+  in mk_alist_reprs R_thm EVAL numSyntax.int_of_term Int.compare end
+
+fun test_mk_alookup ns = let
+    open numSyntax
+    val _ = I
+    fun f i = ((i * 157) mod 1000)
+    fun el i = pairSyntax.mk_pair (term_of_int (f i), term_of_int i)
+  in mk_icomb (alookup_tm, listSyntax.mk_list (map el ns, type_of (el 0))) end
+
+fun test_200 rs = let
+    val al1 = test_mk_alookup (upto 1 200)
+    val al2 = test_mk_alookup [1, 4, 3]
+    val merge = list_mk_icomb (option_choice_tm, [al1, al2])
+  in mk_repr rs merge end
+
+(*
+val rs = test_rs ()
+val thm_200 = timeit "build repr" test_200 rs
+*)
+
+(* proving and using is_lookup thms *)
+
+fun build_lookup (dest : term -> 'a) cmp R k =
+  let
+    val dest_k = dest k
+    fun chk thm = if same_const is_lookup_tm (fst (strip_comb (concl thm)))
+      then thm
+      else (print "Not a lookup_tm:\n"; print_thm thm; print "\n";
+        raise (err "build_lookup" "check"))
+    val pp = chk o assume_prems
+    fun build t = if listSyntax.is_nil t
+      then pp (ISPECL [R, k, t] is_lookup_empty)
+      else if listSyntax.is_cons t then let
+        val (xs, _) = listSyntax.dest_list t
+        val _ = length xs = 1 orelse raise (err "build_insert" "malformed")
+        val (k', v) = pairSyntax.dest_pair (hd xs)
+      in case cmp (dest_k, dest k') of
+          EQUAL => pp (ISPECL [R, k, k', v] is_lookup_hit)
+        | GREATER => pp (ISPECL [R, k, k', v] is_lookup_far_right)
+        | LESS => pp (ISPECL [R, k, k', v] is_lookup_far_left)
+      end else let
+        val (f, xs) = strip_comb t
+        val _ = same_const count_append_tm f
+           orelse raise (err "build_lookup" "unknown")
+        val (n, l, r) = case xs of [n, l, r] => (n, l, r)
+           | _ => raise (err "build_lookup" "num args")
+        fun vsub nm v = [mk_var (nm, type_of v) |-> v]
+      in if not (cmp (dest_k, dest (hd_key r)) = LESS)
+        then do_inst_mp (vsub "l" l) (SPEC n is_lookup_r) (build r)
+        else if cmp (dest_k, dest (last_key l)) = GREATER
+        then pp (ISPECL [R, n, l, r, k] is_lookup_centre)
+        else do_inst_mp (vsub "r" r) (SPEC n is_lookup_l) (build l)
+      end
+  in build end
+
+fun prove_lookup R conv dest cmp k al = let
+    val thm = build_lookup dest cmp R k al
+    fun prove thm = if not (is_imp (concl thm)) then thm
+      else prove (prove_assum_by_conv conv thm)
+  in thm |> DISCH_ALL |> prove end
+
+fun repr_prove_lookup conv dest cmp repr_thm k = let
+    val (f, xs) = strip_comb (concl repr_thm)
+    val f = same_const f repr_tm orelse
+        raise (err "repr_prove_lookup" "unexpected")
+    val (R, al, f) = case xs of [R, al, f] => (R, al, f)
+        | _ => raise (err "repr_prove_lookup" "num args")
+    val lookup = prove_lookup R conv dest cmp k al
+  in MATCH_MP lookup_repr (CONJ repr_thm lookup) end
+
+fun reprs_conv rs tm = let
+    val AList_Reprs inn_rs = rs
+    val (f, x) = dest_comb tm handle HOL_ERR _ => raise UNCHANGED
+    val repr_thm = case peek_repr rs f of
+      NONE => raise UNCHANGED | SOME thm => thm
+  in if is_eq (concl repr_thm)
+    then (RATOR_CONV (REWR_CONV repr_thm) THENC reprs_conv rs) tm
+    else repr_prove_lookup (#conv inn_rs) (#dest inn_rs) (#cmp inn_rs)
+        repr_thm x
+  end
+
+fun extract_test f rs i = mk_comb (f, numSyntax.term_of_int i) |> reprs_conv rs
+
+fun extract_test_1000 rs = let
+    val alookup = test_mk_alookup (upto 1 300)
+    val f = mk_var ("f", type_of alookup)
+    val f_def = new_definition ("f", mk_eq (f, alookup))
+    val res1 = timeit "add def" (add_alist_repr rs) f_def
+    val res2 = timeit "map extract" (map (extract_test f rs)) (upto 1 1000)
+  in res2 end
+
+end
diff --git a/translator/ml_progLib.sml b/translator/ml_progLib.sml
index a668a12a8d..330ac1f305 100644
--- a/translator/ml_progLib.sml
+++ b/translator/ml_progLib.sml
@@ -6,7 +6,7 @@ structure ml_progLib :> ml_progLib =
 struct
 
 open preamble;
-open ml_progTheory astSyntax packLib alist_treeLib comparisonTheory;
+open ml_progTheory astSyntax packLib alist_tree2Lib comparisonTheory;
 local open mlstringSyntax in end;
 
 fun allowing_rebind f = Feedback.trace ("Theory.allow_rebinds", 1) f
@@ -34,7 +34,7 @@ local
 
 val nsLookup_repr_set = let
     val irrefl_thm = MATCH_MP good_cmp_Less_irrefl_trans mlstringTheory.good_cmp_compare
-  in alist_treeLib.mk_alist_reprs irrefl_thm EVAL
+  in alist_tree2Lib.mk_alist_reprs irrefl_thm EVAL
     str_dest (list_compare Int.compare)
   end
 
@@ -107,8 +107,9 @@ val nsLookup_conv_arg1_xs = [boolSyntax.conjunction, boolSyntax.disjunction,
 fun nsLookup_arg1_conv conv tm = let
     val (f, xs) = strip_comb tm
     val _ = exists (same_const f) nsLookup_conv_arg1_xs orelse raise UNCHANGED
-  in if length xs > 1 then RATOR_CONV (nsLookup_arg1_conv conv) tm
-    else if length xs = 1 then RAND_CONV conv tm
+    val len = length xs
+  in if len > 1 then RATOR_CONV (nsLookup_arg1_conv conv) tm
+    else if len = 1 then RAND_CONV conv tm
     else raise UNCHANGED
   end
 
@@ -121,9 +122,10 @@ val nsLookup_rewrs = List.concat (map BODY_CONJUNCTS
         nsLookup_Short_Bind, nsLookup_Mod1_Bind, nsLookup_merge_env_eqs,
         nsLookup_empty_eqs, alistTheory.ALOOKUP_def])
 
+val nsLookup_rewrs_conv = GEN_REWRITE_CONV I Rewrite.empty_rewrites nsLookup_rewrs
+
 fun nsLookup_conv tm = REPEATC (BETA_CONV ORELSEC FIRST_CONV
-  (map REWR_CONV nsLookup_rewrs
-    @ map (RATOR_CONV o REWR_CONV) nsLookup_rewrs
+   ([nsLookup_rewrs_conv,RATOR_CONV nsLookup_rewrs_conv]
     @ map QCHANGED_CONV [nsLookup_arg1_conv nsLookup_conv,
         nsLookup_pf_conv])) tm
 
@@ -273,24 +275,32 @@ fun let_v_abbrev nm conv op_nm (th, ML_code (ss, envs, vs, ml_th)) = let
 (*
 val tm = ``!n. n = 5 ==> n < 8``
 *)
+local
+val conv1 = REWR_CONV UNWIND_FORALL_THM1
+val conv2 = REWR_CONV UNWIND_FORALL_THM2
+in
 fun unwind_forall_conv tm =
   let
     val (v,_) = dest_forall tm
   in
     (QUANT_CONV (RAND_CONV (UNBETA_CONV v))
-     THENC (REWR_CONV UNWIND_FORALL_THM1 ORELSEC
-            REWR_CONV UNWIND_FORALL_THM2)
+     THENC (conv1 ORELSEC conv2)
      THENC BETA_CONV) tm
   end
+end
 
+local
+val conv1 = REWR_CONV SOME_11
+in
 fun forall_nsLookup_upd nm (th,x) =
   (CONV_RULE
     (QUANT_CONV
       ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) (nsLookup_conv THENC EVAL)
-       THENC (RATOR_CONV o RAND_CONV) (REWR_CONV SOME_11))
+       THENC (RATOR_CONV o RAND_CONV) (conv1))
      THENC unwind_forall_conv) th,
    x) handle HOL_ERR _ =>
   failwith "forall_nsLookup_upd: nsLookup failed to produce SOME"
+end
 
 fun solve_ml_imp f nm (th, ML_code code) = let
     val msg = "solve_ml_imp: " ^ nm ^ ": not imp"
diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
index 747841890a..fc61a16410 100644
--- a/translator/ml_translatorLib.sml
+++ b/translator/ml_translatorLib.sml
@@ -11,6 +11,7 @@ open astTheory semanticPrimitivesTheory namespaceTheory;
 open evaluateTheory astSyntax semanticPrimitivesSyntax;
 local open stringLib in end
 open ml_translatorTheory ml_translatorSyntax intLib;
+open ml_translatorTrace
 open arithmeticTheory listTheory combinTheory pairTheory pairLib;
 open integerTheory intLib ml_optimiseTheory ml_pmatchTheory;
 open mlstringLib mlstringSyntax mlvectorSyntax packLib ml_progTheory ml_progLib
@@ -67,8 +68,6 @@ local
      ("PreImp_Eval",``PreImp _ (Eval _ _ _)``),
      ("nsLookup_pat",``nsLookup (env:(α,β,γ) namespace) name``),
      ("pmatch_eq_Match_type_error",``pmatch _ _ _ _ _ = Match_type_error``),
-     ("auto eq proof 1",``!x1:α x2:β x3:γ x4:δ. bbb``),
-     ("auto eq proof 2",``!x1:α x2:β. bbb ==> bbbb``),
      ("remove lookup_cons",``!x1 x2 x3. (lookup_cons x1 x2 = SOME x3) = T``),
      ("no_closure_pat",``!(x:α) v. p x v ==> no_closures v``),
      ("types_match_pat",``!x1:α v1 x2:α v2. p x1 v1 /\ p x2 v2 ==> types_match v1 v2``),
@@ -195,12 +194,27 @@ fun mk_tid name =
       (mlstringSyntax.mk_mlstring name))
 val true_tid = mk_tid "true"
 val false_tid = mk_tid "false"
-val true_exp_tm = (Eval_Val_BOOL_TRUE |> concl |> rator |> rand)
-val false_exp_tm = (Eval_Val_BOOL_FALSE |> concl |> rator |> rand)
+val true_exp_tm = ml_translatorSyntax.TRUE
+val false_exp_tm = ml_translatorSyntax.FALSE
 
+(*
 fun D th = let
   val th = th |> DISCH_ALL |> PURE_REWRITE_RULE [AND_IMP_INTRO]
   in if is_imp (concl th) then th else DISCH T th end
+*)
+local
+val conv = REWR_CONV AND_IMP_INTRO
+in
+fun D th =
+  let
+    val th = HOLset.foldl (fn(asm,th) => DISCH asm th |>
+                                         CONV_RULE (TRY_CONV conv)) th (hypset th)
+  in
+    if is_imp (concl th)
+      then th
+      else DISCH T th
+  end
+end
 
 fun is_const_str str = can prim_mk_const {Thy=current_theory(), Name=str};
 
@@ -359,7 +373,7 @@ in
       val (new_pre,th1) =
         (if is_imp (concl (SPEC_ALL new_pre))
          then (* case: new_pre is an induction theorem *)
-           (((MATCH_MP IMP_EQ_T (MP (D new_pre) TRUTH)
+           (((EQT_INTRO (MP (D new_pre) TRUTH)
              handle HOL_ERR _ => new_pre)
              |> PURE_REWRITE_RULE [GSYM CONJ_ASSOC]),
             PURE_REWRITE_RULE [GSYM CONJ_ASSOC] th1)
@@ -467,9 +481,8 @@ in
   fun mk_cons_name tm =
     let
       val (_, ty) = strip_fun (type_of tm)
-      val info = Option.valOf (TypeBase.fetch ty)
-      val (thyn, tyn) = TypeBasePure.ty_name_of info
-      val name = term_to_string tm
+      val {Thy = thyn,Tyop = tyn,...} = Type.dest_thy_type ty
+      val name = dest_const tm |> fst
     in
       (* separating with underscores is more prone to name clashes *)
       String.concat ["%%", thyn, "%%", tyn, "%%", name, "%%"]
@@ -496,9 +509,9 @@ end
  * current module) we give a Long name, otherwise the name is short.
  *)
 fun full_id n =
-  case lookup_type_mod (mlstringSyntax.dest_mlstring n) of
-    NONE => astSyntax.mk_Short n
-  | SOME type_mod => get_qualified_name type_mod n;
+  case lookup_type_mod n of
+    NONE => astSyntax.mk_Short (mlstringSyntax.mk_mlstring n)
+  | SOME type_mod => get_qualified_name type_mod (mlstringSyntax.mk_mlstring n);
 
 (* code for managing type information *)
 
@@ -553,9 +566,6 @@ fun word_ty_ok ty =
     end
   else false;
 
-val mlstring_ty = mlstringTheory.implode_def |> concl |> rand
-  |> type_of |> dest_type |> snd |> last;
-
 local
   val prim_exn_list = get_term "prim_exn_list"
   val xs = listSyntax.dest_list prim_exn_list |> fst
@@ -593,16 +603,9 @@ in
      type_memory := [];
      deferred_dprogs := [];
      all_eq_lemmas := default_eq_lemmas)
-  fun dest_fun_type ty = let
-    val (name,args) = dest_type ty
-    in if name = "fun" then (el 1 args, el 2 args) else failwith("not fun type") end
+  fun dest_fun_type ty = Type.dom_rng ty
   fun find_type_mapping ty =
     first (fn (t,_) => can (match_type t) ty) (!type_mappings)
-  fun free_typevars ty =
-    if can dest_vartype ty then [ty] else let
-    val (name,tt) = dest_type ty
-    in Lib.flatten (map free_typevars tt) end
-    handle HOL_ERR _ => []
   fun add_new_type_mapping ty target_ty =
     (type_mappings := (ty,target_ty) :: (!type_mappings))
   fun string_tl s = s |> explode |> tl |> implode
@@ -614,7 +617,8 @@ in
   val word64_ast_t = prim_type "word64"
   val string_ast_t = prim_type "string"
   val double_ast_t = prim_type "double"
-
+  val mk_list_ast_t = let val id_tm = astSyntax.mk_Short(mlstringSyntax.mk_mlstring "list")
+                      in fn tm => Atapp [tm] id_tm end
   val one_ast_t = mk_Attup(listSyntax.mk_list([],ast_t_ty))
   fun type2t ty =
     if ty = bool then bool_ast_t else
@@ -628,31 +632,29 @@ in
     if ty = stringSyntax.char_ty then char_ast_t else
     if ty = oneSyntax.one_ty then one_ast_t else
     if use_hol_string_type() andalso ty = stringSyntax.string_ty then string_ast_t else
-    if ty = mlstring_ty then string_ast_t else
+    if ty = mlstringSyntax.mlstring_ty then string_ast_t else
     if ty = float64_ty then double_ast_t else
+    if can listSyntax.dest_list_type ty then mk_list_ast_t (type2t(listSyntax.dest_list_type ty)) else
+    if can Type.dom_rng ty then
+       let val (ty1,ty2) = Type.dom_rng ty
+       in mk_Atfun (type2t ty1,type2t ty2) end else
+    if can pairSyntax.dest_prod ty then
+       let val (ty1,ty2) = pairSyntax.dest_prod ty
+       in mk_Attup(listSyntax.mk_list([type2t ty1,type2t ty2],astSyntax.ast_t_ty)) end else
     if can dest_vartype ty then
       astSyntax.mk_Atvar(mlstringSyntax.mk_mlstring (dest_vartype ty))
     else let
       val (lhs,rhs) = find_type_mapping ty
-      val i = match_type lhs ty
-      val xs = free_typevars rhs
-      val i = filter (fn {redex = a, residue = _} => mem a xs) i
-      val tm = type2t rhs
-      val s = map (fn {redex = a, residue = b} => type2t a |-> type2t b) i
-      in subst s tm end handle HOL_ERR _ =>
+      val i = match_type ty lhs
+      val rhs' = type_subst i rhs
+      in type2t rhs' end handle HOL_ERR _ =>
     let
-      val (x,tt) = dest_type ty
-      val name = if x = "fun" then "fun" else
-                 if x = "prod" then "prod" else
-                   full_name_of_type ty
+      val (_,tt) = dest_type ty
+      val name = full_name_of_type ty
       val tt = map type2t tt
-      val name_tm = mlstringSyntax.mk_mlstring name
-      in if name = "fun"  then mk_Atfun(el 1 tt, el 2 tt) else
-         if name = "prod" then mk_Attup(listSyntax.mk_list(tt,astSyntax.ast_t_ty)) else
-         if name = "list" then Atapp tt (astSyntax.mk_Short(name_tm))
-                          else Atapp tt (full_id name_tm) end
-  val HOL_STRING_TYPE =
-    HOL_STRING_TYPE_def |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator
+    in
+      Atapp tt (full_id name)
+    end
   fun inst_type_inv (ty,inv) ty0 = let
     val i = match_type ty ty0
     val ii = map (fn {redex = x, residue = y} => (x,y)) i
@@ -682,9 +684,12 @@ in
     if ty = mlstringSyntax.mlstring_ty then STRING_TYPE else
     if ty = float64_ty then FLOAT64 else
     if is_vector_type ty then let
-      val inv = get_type_inv (dest_vector_type ty)
-      in VECTOR_TYPE_def |> ISPEC inv |> SPEC_ALL
-         |> concl |> dest_eq |> fst |> rator |> rator end
+      val a_ty = dest_vector_type ty
+      val inv = get_type_inv (a_ty)
+      val VECTOR_TYPE = prim_mk_const{Thy="ml_translator",Name="VECTOR_TYPE"}
+      in
+        mk_comb(inst[Type.alpha|->a_ty] VECTOR_TYPE,inv)
+      end
     else
       list_inst_type_inv ty (!other_types)
       handle HOL_ERR _ => raise UnsupportedType ty
@@ -778,9 +783,8 @@ fun get_unique_name str = let
   val initial_name = if size initial_name = 0 then "f" else initial_name
   in find_new_name initial_name end
 
-fun dest_args tm =
-  let val (x,y) = dest_comb tm in dest_args x @ [y] end
-  handle HOL_ERR _ => []
+fun dest_args tm = strip_comb tm
+                 |> snd
 
 fun allowing_rebind f = Feedback.trace ("Theory.allow_rebinds", 1) f
 
@@ -868,6 +872,7 @@ fun timing_message msg = case ! trace_timing_to of
 
 fun start_timing nm = case ! trace_timing_to of
   SOME fname => let
+    val nm = nm ()
     val time = Portable.timestamp ()
     val f = TextIO.openAppend fname
     val time_s = Portable.time_to_string time
@@ -1000,8 +1005,8 @@ fun get_nchotomy_of ty = let (* ensures that good variables names are used *)
   in lemma end
 
 fun find_mutrec_types ty = let (* e.g. input ``:v`` gives [``:exp``,``:v``]  *)
-  fun is_pair_ty ty = fst (dest_type ty) = "prod"
-  val xs = TypeBase.axiom_of ty |> SPEC_ALL  |> concl |> strip_exists |> #1 |> map (#1 o dest_fun_type o type_of) |> (fn ls => filter (fn ty => intersect ((#2 o dest_type) ty) ls = []) ls)
+  fun is_pair_ty ty = can pairSyntax.dest_prod ty
+  val xs = TypeBase.axiom_of ty |> SPEC_ALL  |> concl |> strip_exists |> #1 |> map (#1 o Type.dom_rng o type_of) |> (fn ls => filter (fn ty => intersect ((#2 o dest_type) ty) ls = []) ls)
   in if is_pair_ty ty then [ty] else if length xs = 0 then [ty] else xs end
 
 (*
@@ -1077,12 +1082,12 @@ fun derive_record_specific_thms ty = let
     |> map (rator o rator o fst o dest_eq o concl o SPEC_ALL)
   val thy_name = access_funs |> hd |>dest_thy_const |> #Thy
   val tm =
-    DB.fetch thy_name (ty_name ^ "_11")
+    TypeBase.one_one_of ty
     |> SPEC_ALL |> concl |> dest_eq |> fst |> dest_eq |> fst
   val xs = dest_args tm
   val c = repeat rator tm
   val case_tm =
-    DB.fetch thy_name (ty_name ^ "_case_cong")
+    TypeBase.case_cong_of ty
     |> SPEC_ALL |> UNDISCH_ALL |> concl |> dest_eq |> fst |> repeat rator
   fun prove_accessor_eq (a,x) = let
     val v = mk_var("v",type_of tm)
@@ -1254,10 +1259,11 @@ fun mk_EqualityType_ind typ = let
         |> map (fst o strip_comb)
         |> filter is_const
         |> HOLset.fromList Term.compare |> HOLset.listItems
-        |> map guess_const_def
-    val ss = list_ss ++ simpLib.type_ssfrag v_ty ++ optionSimps.OPTION_ss
+        |> mapfilter guess_const_def
+    val ty_inv_defs = ml_translatorTheory.LIST_TYPE_def :: ty_inv_defs 
+    val ss = list_ss ++ simpLib.type_ssfrag semanticPrimitivesSyntax.v_ty ++ optionSimps.OPTION_ss
         ++ simpLib.type_ssfrag (pairSyntax.mk_prod (alpha, beta))
-        ++ simpLib.type_ssfrag stamp_ty ++ stringSimps.STRING_ss
+        ++ simpLib.type_ssfrag semanticPrimitivesSyntax.stamp_ty ++ stringSimps.STRING_ss
         ++ BasicProvers.thy_ssfrag "mlstring" ++ simpLib.type_ssfrag mlstringSyntax.mlstring_ty
     fun adj tm = if not (is_Conv tm) then snd (strip_comb tm)
         else dest_Conv tm |> snd |> listSyntax.dest_list |> fst
@@ -1274,8 +1280,26 @@ fun mk_EqualityType_ind typ = let
       in insts (hd ys) (tl ys) end)
     val gl = map (ml_translatorSyntax.mk_EqualityType o get_type_inv) proof_tys
         |> list_mk_conj
+    fun is_same (asl,g) = 
+        let  val case_tm = g
+                         |> strip_forall |> snd
+                         |> dest_imp |> fst
+             val xs = (pairSyntax.spine_pair o markerSyntax.dest_Case) case_tm
+             val (l,r) = ((fst o strip_comb) ## (fst o strip_comb)) (el 1 xs,el 2 xs)
+             val () = if is_const l andalso is_const r
+                      then () else failwith("is_different expected 2 constants")
+        in
+             if same_const l r then ALL_TAC (asl,g)
+             else NO_TAC (asl,g)
+        end
     val assums = map (ml_translatorSyntax.mk_EqualityType o get_type_inv) ex_assum_tys
     val prop = mk_imp (list_mk_conj (T :: assums), gl)
+    val typs = find_mutrec_types typ
+    val inj_ss = List.foldl (fn (typ,acc) => acc ++ simpLib.type_ssfrag typ)
+                 (bool_ss) (listSyntax.mk_list_type Type.alpha :: typs)
+    (*
+    val _ = set_goal ([],prop)
+    *)
     val thm = prove (prop,
         disch_tac
         \\ REWRITE_TAC [EqualityType_eq_at]
@@ -1283,16 +1307,23 @@ fun mk_EqualityType_ind typ = let
         \\ rpt strip_tac
         \\ REWRITE_TAC [EqualityType_at_eq_Case_rearranged]
         \\ Cases
-        \\ simp_tac ss (ty_inv_defs @ [PULL_EXISTS, types_match_def,
-            semanticPrimitivesTheory.ctor_same_type_def,
-            semanticPrimitivesTheory.lit_same_type_def,
-            semanticPrimitivesTheory.same_type_def, no_closures_def])
-        \\ TRY (simp_tac (bool_ss ++ simpLib.type_ssfrag typ) [] \\ NO_TAC)
-        \\ rpt (gen_tac ORELSE disch_tac)
-        \\ full_simp_tac ss []
-        \\ rpt fiddle_case_tac
-        \\ full_simp_tac ss [EqualityType_eq_at, markerTheory.Case_def]
-        \\ simp_tac (bool_ss ++ simpLib.type_ssfrag typ) []
+        \\ IF is_same
+            (simp_tac ss (ty_inv_defs @ [PULL_EXISTS, types_match_def,
+             semanticPrimitivesTheory.ctor_same_type_def,
+             semanticPrimitivesTheory.lit_same_type_def,
+             semanticPrimitivesTheory.same_type_def, no_closures_def])
+             \\ TRY (simp_tac (inj_ss) [] \\ NO_TAC)
+             \\ rpt (gen_tac ORELSE disch_tac)
+             \\ full_simp_tac ss []
+             \\ rpt fiddle_case_tac
+             \\ full_simp_tac ss [EqualityType_eq_at, markerTheory.Case_def]
+             \\ simp_tac (inj_ss) [])
+            (rpt gen_tac
+             \\ simp_tac (inj_ss) []
+             \\ disch_tac
+             \\ CONV_TAC (LAND_CONV (PURE_ONCE_REWRITE_CONV ty_inv_defs))
+             \\ DISCH_THEN (REPEAT_TCL STRIP_THM_THEN (fn x => SUBST_ALL_TAC x ORELSE ASSUME_TAC x))
+             \\ EVAL_TAC)
     )
   in (assums, thm) end
   handle
@@ -1356,7 +1387,7 @@ fun define_v_fun ty = let
         |> map (fst o strip_comb)
         |> filter is_const
         |> HOLset.fromList Term.compare |> HOLset.listItems
-        |> map guess_const_def
+        |> mapfilter guess_const_def
     fun name ty = get_type_inv ty |> strip_comb |> fst |> dest_const |> fst
         |> Portable.replace_string {from = "_TYPE", to = "_v"}
     fun is_aux ty = exists (not o is_vartype) (snd (dest_type ty))
@@ -1403,6 +1434,7 @@ fun define_v_fun ty = let
         |> map (fn ty => mk_imp (asms, mk_is_tr ty))
         |> map (fn gl => prove (gl, disch_tac \\ mp_tac thm \\ asm_simp_tac bool_ss []))
   end
+  handle (e as HOL_ERR _) => raise (wrap_exn "ml_translatorLib" "define_v_fun" e);
 
 fun define_type_reps [] = []
   | define_type_reps (ty :: tys) = let
@@ -1660,7 +1692,7 @@ fun avoid_v_subst ty = let
 
 fun derive_thms_for_type is_exn_type ty = let
 
-  val start = start_timing "derive_thms_for_type"
+  val start = start_timing (fn () => "derive_thms_for_type")
   val tsubst = avoid_v_subst ty;
   val ty = type_subst tsubst ty;
   val is_word_type = wordsSyntax.is_word_type ty
@@ -1779,7 +1811,7 @@ val th = inv_defs |> map #2 |> hd
 *)
   (* prove lemma for case_of *)
   fun prove_case_of_lemma (ty,case_th,inv_lhs,inv_def) = let
-    val start = start_timing ("prove_case_of_lemma for "
+    val start = start_timing (fn () => "prove_case_of_lemma for "
         ^ Parse.type_to_string ty)
     val cases_th = TypeBase.case_def_of ty |> INST_TYPE tsubst
     val (x1,x2) = cases_th |> CONJUNCTS |> hd |> concl |> repeat (snd o dest_forall)
@@ -1804,17 +1836,14 @@ val th = inv_defs |> map #2 |> hd
     val input_var = filter (fn x => not (tmem x (free_vars cases_tm))) (free_vars exp) |> hd
     val ret_ty = type_of exp
     val xs = rev (map rand (find_terms is_eq (concl case_th)))
-    fun add_nums [] = []
-      | add_nums (x::xs) = (x,length xs+1) :: add_nums xs
-    val ys = rev (add_nums (rev (zip (map snd vs) xs)))
+    fun add_nums xs = mapi (fn i => fn x => (x,i + 1)) xs
+    val ys = add_nums (zip (map snd vs) xs)
     fun str_tl s = implode (tl (explode s))
-    fun list_app x [] = x
-      | list_app x (y::ys) = list_app (mk_comb(x,y)) ys
-    val start_mk_vars = start_timing "mk_vars"
+    val start_mk_vars = start_timing (fn () => "mk_vars")
     fun mk_vars ((f,tm),n) = let
       val xs = rev (free_vars tm)
-      val fxs = list_app f xs
-      val pxs = list_app (mk_var("b" ^ int_to_string n,list_mk_type xs bool)) xs
+      val fxs = list_mk_comb(f, xs)
+      val pxs = list_mk_comb(mk_var("b" ^ int_to_string n,list_mk_type xs bool), xs)
       val xs = map (fn x => let val s = str_tl (fst (dest_var x)) in
                             (x,mk_var("n" ^ s,mlstringSyntax.mlstring_ty),
                                mk_var("v" ^ s,v_ty)) end) xs
@@ -1897,11 +1926,16 @@ val (n,f,fxs,pxs,tm,exp,xs) = el 1 ts
     val goal = mk_imp(type_assum,mk_imp(tt,mk_imp(hyps,result)))
     val Mat_lemma = ISPEC (rator x) IMP_Eval_Mat_cases |> SPEC input_var
     val is_simple_case = name = "PAIR_TYPE" orelse name = "UNIT_TYPE"
+    fun TAG_X_ASSUM tm ttac =
+        PRED_ASSUM (fn x => is_TAG x andalso dest_TAG x |> fst |> same_const tm)
+                   (ttac o CONV_RULE (REWR_CONV TAG_def))
 (*
-  set_goal([],goal)
+    val _ = set_goal([],goal)
 *)
+
     val case_lemma = auto_prove "case-of-proof" (goal,
-      rpt strip_tac
+      disch_then (markerLib.assume_named_tac "lookup_cons")
+      \\ rpt strip_tac
       \\ match_mp_tac Mat_lemma
       \\ conj_tac THEN1
        (pop_assum mp_tac
@@ -1914,17 +1948,36 @@ val (n,f,fxs,pxs,tm,exp,xs) = el 1 ts
       \\ CONV_TAC (DEPTH_CONV BETA_CONV)
       \\ (if is_simple_case then all_tac else (conj_tac THEN1 EVAL_TAC))
       \\ conj_tac THEN1
-       (asm_simp_tac std_ss [good_cons_env_def,EVERY_DEF,LENGTH,
-          HD,LET_THM,pat_bindings_def,MAP]
-        \\ once_rewrite_tac [GSYM ALL_DISTINCT_REVERSE]
-        \\ asm_simp_tac std_ss [REVERSE_DEF,APPEND] \\ EVAL_TAC)
-      \\ Cases_on `^input_var` \\ rewrite_tac [inv_def]
+       (if is_simple_case
+          then 
+          (asm_simp_tac std_ss [EVERY_DEF,LENGTH,
+          HD,LET_THM,pat_bindings_def,MAP,markerLib.L "lookup_cons"]
+          \\ once_rewrite_tac [GSYM ALL_DISTINCT_REVERSE]
+          \\ asm_simp_tac std_ss [REVERSE_DEF,APPEND] \\ EVAL_TAC)
+          else
+          ((CONV_TAC (REWR_CONV good_cons_env_def))
+          \\ conj_tac
+          THEN1
+          (asm_simp_tac std_ss [EVERY_DEF,LENGTH,
+          HD,LET_THM,pat_bindings_def,MAP,markerLib.L "lookup_cons"]
+          \\ once_rewrite_tac [GSYM ALL_DISTINCT_REVERSE]
+          \\ asm_simp_tac std_ss [REVERSE_DEF,APPEND] \\ EVAL_TAC)
+          \\ EVAL_TAC)
+          )
+      \\ Cases_on `^input_var`
+      \\ GEN_TAC
+      \\ CONV_TAC (LAND_CONV (PURE_ONCE_REWRITE_CONV [inv_def]))
+      \\ DISCH_THEN (REPEAT_TCL STRIP_THM_THEN (fn x => SUBST_ALL_TAC x ORELSE ASSUME_TAC x))
+      \\ irule_at (Pos hd) EQ_REFL
+      \\ CONV_TAC (STRIP_QUANT_CONV (LAND_CONV EVAL))
       \\ simp_tac std_ss [mlstringTheory.mlstring_11,v_11,MEM,stamp_11,CONS_11,ZIP,write_list_def,
-           stringTheory.CHR_11,LENGTH,NOT_NIL_CONS,NOT_CONS_NIL,PULL_EXISTS]
+           stringTheory.CHR_11,LENGTH,NOT_NIL_CONS,NOT_CONS_NIL]
       \\ simp_tac (srw_ss()) [cases_th]
-      \\ rpt (pop_assum mp_tac) \\ rewrite_tac [TAG_def,CONTAINER_def]
-      \\ rpt strip_tac
-      \\ first_x_assum match_mp_tac \\ fs [])
+      \\ first_x_assum (match_mp_tac o CONV_RULE (REWR_CONV TAG_def))
+      \\ TAG_X_ASSUM oneSyntax.one_tm  
+             (asm_simp_tac (srw_ss()) o single o
+              PURE_REWRITE_RULE[CONTAINER_def])
+      \\ full_simp_tac(srw_ss()) [])
     val case_lemma = case_lemma |> PURE_REWRITE_RULE [TAG_def,Mat_cases_def,MAP]
                        |> CONV_RULE (DEPTH_CONV (PairRules.PBETA_CONV))
     val _ = end_timing start
@@ -2052,7 +2105,7 @@ local
     (* if abstract_mode then add_deferred_dprog dprog else *)
     ml_prog_update (add_prog dprog I)
   fun add_type abstract_mode ty = let
-    val start = start_timing ("adding type " ^ Parse.type_to_string ty)
+    val start = start_timing (fn () => "adding type " ^ Parse.type_to_string ty)
     val fcps = ((filter fcpSyntax.is_numeric_type) o snd o dest_type) ty
     val (rws1,rws2,res,tr_lemmas,dprog) = derive_thms_for_type false ty
     val (rws1,rws2) =
@@ -2096,11 +2149,11 @@ in
     in (case_lemma) end
   fun store_eq_thm th = (add_eq_lemma th; th)
   fun register_exn_type_main abstract_mode ty = let
-    val start = start_timing ("adding exn type " ^ Parse.type_to_string ty)
+    val start = start_timing (fn () => "adding exn type " ^ Parse.type_to_string ty)
     val (rws1,rws2,res,tr_lemmas,dprog) = derive_thms_for_type true ty
     val _ = store_dprog abstract_mode dprog
-    val _ = do_timing "add_type_thms" add_type_thms (rws1,rws2,res,tr_lemmas)
-    val _ = do_timing "map do_translate rws1" (map do_translate) rws1
+    val _ = do_timing (fn () => "add_type_thms") add_type_thms (rws1,rws2,res,tr_lemmas)
+    val _ = do_timing (fn () => "map do_translate rws1") (map do_translate) rws1
     val _ = end_timing start
     in () end
   val register_exn_type = register_exn_type_main false
@@ -2118,7 +2171,7 @@ fun register_term_types register_type tm = let
                       @ get_user_supplied_types ()
   fun ignore_type ty =
     if can (first (fn ty1 => can (match_type ty1) ty)) special_types then true else
-    if not (can dest_type ty) then true else
+    if is_vartype ty then true else
     if can (dest_fun_type) ty then true else
     if fcpSyntax.is_numeric_type ty andalso fcpSyntax.dest_int_numeric_type ty > 1 then true else false
   fun typeops ty = let
@@ -2396,7 +2449,7 @@ fun prove_EvalPatBind goal hol2deep = let
   val vs = find_terms is_var_assum (concl th |> rator)
   val vs' = filter (is_var o rand o rand) vs
   fun delete_var tm =
-    if tmem tm vs' then MATCH_MP IMP_EQ_T (ASSUME tm) else NO_CONV tm
+    if tmem tm vs' then EQT_INTRO (ASSUME tm) else NO_CONV tm
   val th = CONV_RULE (RATOR_CONV (DEPTH_CONV delete_var)) th
   val th = CONV_RULE ((RATOR_CONV o RAND_CONV)
               (PairRules.UNPBETA_CONV vars)) th
@@ -2770,7 +2823,7 @@ fun split_let_and_conv tm = let
                           THEN REWRITE_TAC [])
   in lemma end handle HOL_ERR _ => NO_CONV tm;
 
-fun mk_fun_type ty1 ty2 = mk_type("fun",[ty1,ty2])
+fun mk_fun_type ty1 ty2 = ty1 --> ty2
 
 fun list_mk_fun_type [ty] = ty
   | list_mk_fun_type (ty1::tys) =
@@ -2833,9 +2886,7 @@ fun get_induction_for_def def = let
     val step = mk_abs(v,list_mk_forall(xs @ ys,prop))
     in (P,(goal,step)) end
   val res = map goal_step xs
-  fun ISPEC_LIST [] th = th
-    | ISPEC_LIST (x::xs) th = ISPEC_LIST xs (ISPEC x th)
-  val ind = ISPEC_LIST (map (snd o snd) res) raw_ind
+  val ind = ISPECL (map (snd o snd) res) raw_ind
             |> CONV_RULE (DEPTH_CONV BETA_CONV)
   val goal1 = ind |> concl |> dest_imp |> snd
   val goal2 = list_mk_conj (map (fst o snd) res)
@@ -2912,7 +2963,8 @@ val builtin_terops =
   [Eval_substring,
    Eval_FLOAT_FMA]
   |> map (fn th =>
-      (th |> SPEC_ALL |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator |> rator, th))
+      let val th = SPEC_ALL th in
+      (th |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator |> rator, th) end)
 
 val builtin_binops =
   [Eval_NUM_ADD,
@@ -2969,7 +3021,8 @@ val builtin_binops =
    Eval_Implies,
    Eval_pure_seq]
  |> map (fn th =>
-      (th |> SPEC_ALL |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator, th))
+      let val th = SPEC_ALL th in
+      (th |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator, th) end)
 
 val builtin_monops =
   [Eval_implode,
@@ -2998,10 +3051,10 @@ val builtin_monops =
 
 val builtin_hol_string_binops =
   [Eval_HOL_STRING_EL,
-   Eval_HOL_STRING_CONS,
    Eval_HOL_STRING_APPEND]
   |> map (fn th =>
-      (th |> SPEC_ALL |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator, th))
+      let val th = SPEC_ALL th in
+      (th |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator, th) end)
 
 val builtin_hol_string_monops =
   [Eval_HOL_STRING_LENGTH,
@@ -3017,7 +3070,8 @@ val builtin_hol_string_monops =
 val builtin_sub_check =
   [Eval_NUM_SUB_check']
  |> map (fn th =>
-      (th |> SPEC_ALL |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator, th))
+      let val th = SPEC_ALL th in
+      (th |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator, th) end)
 
 val AUTO_ETA_EXPAND_CONV = let (* K ($=) --> K (\x y. x = y) *)
   val must_eta_expand_ops =
@@ -3056,8 +3110,8 @@ val AUTO_ETA_EXPAND_CONV = let (* K ($=) --> K (\x y. x = y) *)
 
 fun force_eqns def = let
   fun f th = if is_eq (concl (SPEC_ALL th)) then th else
-               GEN_ALL (MATCH_MP IMP_EQ_F (SPEC_ALL th)) handle HOL_ERR _ =>
-               GEN_ALL (MATCH_MP IMP_EQ_T (SPEC_ALL th))
+               GEN_ALL (EQF_INTRO (SPEC_ALL th)) handle HOL_ERR _ =>
+               GEN_ALL (EQT_INTRO (SPEC_ALL th))
   in LIST_CONJ (map f (CONJUNCTS (SPEC_ALL def))) end
 
 val use_mem_intro = ref false;
@@ -3233,7 +3287,7 @@ fun move_Eval_conv tm =
     val tm2 = #2 (dest_imp tm1) handle HOL_ERR _ => tm1
   in
     if is_Eval tm2 then
-      MATCH_MP IMP_EQ_T (ASSUME tm)
+      EQT_INTRO (ASSUME tm)
     else NO_CONV tm
   end
 
@@ -3243,7 +3297,7 @@ val be_quiet = true
 *)
 
 fun clean_assumptions_aux be_quiet th = let
-  val start = start_timing "clean assumptions"
+  val start = start_timing (fn () => "clean assumptions")
   val lhs1 = get_term "nsLookup_pat"
   val pattern1 = mk_eq(lhs1,mk_var("_",type_of lhs1))
   val lhs2 = lookup_cons_def (*lookup_cons_thm*) |> SPEC_ALL |> concl |> dest_eq |> fst
@@ -3324,6 +3378,7 @@ fun MY_MATCH_MP th1 th2 = let
   in MP (INST s (INST_TYPE i th1)) th2 end;
 
 fun force_remove_fix thx = let
+  (* TODO lift out pat*)
   val pat = Eq_def |> SPEC_ALL |> concl |> dest_eq |> fst
   val xs = map rand (find_terms (can (match_term pat)) (concl thx))
   val s = SIMP_RULE std_ss [Eval_FUN_FORALL_EQ,FUN_QUANT_SIMP]
@@ -3443,6 +3498,9 @@ fun is_float_literal tm =
     end handle HOL_ERR _ => false
 
 fun hol2deep tm =
+  let
+    val _ = ml_translatorTrace.trace(4, LZ_TEXT (fn () => "hol2deep: " ^ Parse.term_to_string tm))
+  in
   (* variables *)
   if is_var tm then let
     val (name,ty) = dest_var tm
@@ -3484,9 +3542,36 @@ fun hol2deep tm =
   if (tm ~~ TRUE) then Eval_Val_BOOL_TRUE else
   if (tm ~~ FALSE) then Eval_Val_BOOL_FALSE else
   (* data-type constructor *)
-  inst_cons_thm tm hol2deep handle HOL_ERR _ =>
+  if use_hol_string_type () andalso type_of tm = stringSyntax.string_ty
+     andalso can listSyntax.dest_cons tm then
+     let
+       val (x1,x2) = listSyntax.dest_cons tm
+       val th1 = hol2deep x1
+       val th2 = hol2deep x2
+       val result = (MATCH_MP Eval_HOL_STRING_CONS (CONJ th1 th2))
+                  |> UNDISCH_ALL
+     in
+       check_inv "HOL_STRING_CONS" tm result
+     end else
+  if can cons_for tm then inst_cons_thm tm hol2deep else
+  (* if statements *)
+  if is_cond tm then
+    if is_precond (tm |> rator |> rator |> rand) then let
+      val (x1,x2,x3) = dest_cond tm
+      val th2 = hol2deep x2
+      val lemma = IF_TAKEN |> SPEC x1 |> ISPEC x2 |> SPEC x3 |> UNDISCH |> SYM
+      val result = th2 |> CONV_RULE ((RAND_CONV o RAND_CONV) (K lemma))
+      in check_inv "if" tm result end
+    else let
+      val (x1,x2,x3) = dest_cond tm
+      val th1 = hol2deep x1
+      val th2 = hol2deep x2
+      val th3 = hol2deep x3
+      val th = MATCH_MP Eval_If (LIST_CONJ [D th1, D th2, D th3])
+      val result = UNDISCH th
+      in check_inv "if" tm result end else
   (* data-type pattern-matching *)
-  inst_case_thm tm hol2deep handle HOL_ERR _ =>
+  if can TypeBase.dest_case tm then inst_case_thm tm hol2deep else
   (* recursive pattern *)
   if can match_rec_pattern tm then let
     val (lhs,fname,pre_var) = match_rec_pattern tm
@@ -3515,6 +3600,7 @@ fun hol2deep tm =
     val result = apply_arrow h ys
     in check_inv "rec_pattern" tm result end else
   (* previously translated term *)
+  if can lookup_abs_v_thm tm then
   let
     val th = lookup_abs_v_thm tm
     val _ = check_no_ind_assum tm th
@@ -3524,7 +3610,7 @@ fun hol2deep tm =
     val (ss,ii) = match_term res target handle HOL_ERR _ =>
                   match_term (rm_fix res) (rm_fix target) handle HOL_ERR _ => ([],[])
     val result = INST ss (INST_TYPE ii th)
-  in check_inv "lookup_abs_v_thm" tm result end handle NotFoundVThm _ =>
+  in check_inv "lookup_abs_v_thm" tm result end else
   (* previously translated term *)
   if can lookup_v_thm tm then let
     val th = lookup_v_thm tm
@@ -3559,7 +3645,7 @@ fun hol2deep tm =
     val th1 = hol2deep x1
     val th2 = hol2deep x2
     val th3 = hol2deep x3
-    val result = MATCH_MP (MATCH_MP (MATCH_MP lemma th1) (UNDISCH_ALL th2)) (UNDISCH_ALL th3) |> UNDISCH_ALL
+    val result = MATCH_MP lemma (LIST_CONJ [th1, th2 ,th3]) |> UNDISCH_ALL
     in check_inv "terop" tm result end else
   (* equality: n = 0 *)
   if can (match_term (get_term "n = 0")) tm then let
@@ -3578,7 +3664,8 @@ fun hol2deep tm =
     val (p,x1,x2,lemma) = dest_builtin_binop tm
     val th1 = hol2deep x1
     val th2 = hol2deep x2
-    val result = MATCH_MP (MATCH_MP lemma th1) (UNDISCH_ALL th2) |> UNDISCH_ALL
+    val result = (MATCH_MP lemma (CONJ th1 th2))
+               |> UNDISCH_ALL
     in check_inv "binop" tm result end else
   (* built-in unary operations *)
   if can dest_builtin_monop tm then let
@@ -3608,22 +3695,6 @@ fun hol2deep tm =
     val th = MATCH_MP Eval_Or (LIST_CONJ [D th1, D th2])
     val result = UNDISCH th
     in check_inv "or" tm result end else
-  (* if statements *)
-  if is_cond tm then
-    if is_precond (tm |> rator |> rator |> rand) then let
-      val (x1,x2,x3) = dest_cond tm
-      val th2 = hol2deep x2
-      val lemma = IF_TAKEN |> SPEC x1 |> ISPEC x2 |> SPEC x3 |> UNDISCH |> SYM
-      val result = th2 |> CONV_RULE ((RAND_CONV o RAND_CONV) (K lemma))
-      in check_inv "if" tm result end
-    else let
-      val (x1,x2,x3) = dest_cond tm
-      val th1 = hol2deep x1
-      val th2 = hol2deep x2
-      val th3 = hol2deep x3
-      val th = MATCH_MP Eval_If (LIST_CONJ [D th1, D th2, D th3])
-      val result = UNDISCH th
-      in check_inv "if" tm result end else
   (* Num (ABS i) *)
   if can (match_term Num_ABS_pat) tm then let
     val x1 = tm |> rand |> rand
@@ -3727,6 +3798,7 @@ fun hol2deep tm =
     val th2 = INST [v|->z] th2
     val result = MATCH_MP Eval_Let (CONJ th1 th2)
     in check_inv "let" tm result end else
+  (* TODO stop recursively case spliting *)
   (* special pattern *) let
     fun pat_match pat tm = (match_term pat tm; rator pat)
     val r = pat_match MAP_pattern tm handle HOL_ERR _ =>
@@ -3789,6 +3861,7 @@ fun hol2deep tm =
     val result = auto_prove"hol2deep"(goal,SIMP_TAC std_ss [PRECONDITION_def]) |> UNDISCH
     in check_inv "arb" tm result end
   else raise (UnableToTranslate tm)
+  end
 
 fun hol2val tm = let
   val th_rhs = hol2deep tm
@@ -4037,7 +4110,7 @@ val last_const = ref T;
 fun find_def_for_const_wrapper tm = let
     val _ = last_const := tm;
     val _ = is_const tm orelse raise (UnableToTranslate tm)
-    val msg = "find_def_for_const: " ^ fst (dest_const tm)
+    val msg = (fn () => "find_def_for_const: " ^ fst (dest_const tm))
     val def = do_timing msg (! find_def_for_const) tm
     val _ = can (find_term (same_const tm)) (concl def)
         orelse failwith ("find_def_for_const_wrapper: bad def: " ^
@@ -4327,11 +4400,11 @@ val def = (miscTheory.arith_shift_right_def
 
 fun translate_main options translate register_type def = (let
 
-  val start = start_timing "translate_main"
+  val start = start_timing (fn () => "translate_main")
   val original_def = def
   fun the (SOME x) = x | the _ = failwith("the of NONE")
   (* preprocessing: reformulate def, read off info and register types *)
-  val prep_start = start_timing "preprocessing+registering"
+  val prep_start = start_timing (fn () => "preprocessing+registering")
   val _ = register_term_types register_type (concl def)
   val (is_rec,defs,ind) = preprocess_def def
   (* this is usually a no-op, but preprocess_def might have introduced pairs *)
@@ -4359,8 +4432,8 @@ val _ = map (fn (fname,ml_name,lhs,_,_) => install_rec_pattern lhs fname) info
 val (fname,ml_name,lhs,rhs,def) = el 1 info
 can (find_term is_arb) (rhs |> rand |> rator)
 *)
-  val thms = do_timing "doing loop" loop info
-  val thms = do_timing "instantiating cons names"
+  val thms = do_timing (fn () => "doing loop") loop info
+  val thms = do_timing (fn () => "instantiating cons names")
     (map (fn (x0,x1,th,x2) => (x0,x1,instantiate_cons_name th,x2))) thms
 
   val _ = print ("Translating " ^ msg ^ "\n")
@@ -4383,9 +4456,9 @@ val (fname,ml_fname,th,def) = hd thms
                     last rev_params)
     in (fname,ml_fname,def,th,v) end
     handle (e as HOL_ERR _) => raise (wrap_exn "ml_translatorLib" "optimise_and_abstract" e)
-  val thms = do_timing "optimise+abstract" (map optimise_and_abstract) thms
+  val thms = do_timing (fn () => "optimise+abstract") (map optimise_and_abstract) thms
   (* final phase: extract precondition, perform induction, store cert *)
-  val start_fin = start_timing "translate_main final phase"
+  val start_fin = start_timing (fn () => "translate_main final phase")
 
   val (is_fun,results) = if not is_rec then let
     (* non-recursive case *)
@@ -4417,6 +4490,8 @@ val (fname,ml_fname,th,def) = hd thms
         |> SPEC (mlstringSyntax.mk_mlstring ml_fname)
         |> UNDISCH
       else th
+    (* clean up *)
+    val _ = (delete_const o fst o dest_const o fst o dest_eq o concl) code_def
     in
       (is_fun,[(fname,ml_fname,def,th,pre)])
     end
@@ -4566,20 +4641,20 @@ val options = [NoInd]
 
 fun translate_options options def =
   let
-    val start = start_timing "translation"
+    val start = start_timing (fn () => "translation")
 
     val (is_rec,is_fun,results) =
       translate_main options (translate_options options) register_type def
 
     val () =
       if !generate_sigs then
-        let val _ = do_timing "generate_sig_thms" generate_sig_thms results
+        let val _ = do_timing (fn () => "generate_sig_thms") generate_sig_thms results
         in () end
       else ()
   in
     if is_rec then
     let
-      val start_rec = start_timing "processing rec case"
+      val start_rec = start_timing (fn () => "processing rec case")
       val recc = results |> map (fn (fname,_,def,th,pre) => th) |> hd |> hyp
         |> first (can (find_term (aconv Recclosure_tm)))
         |> rand |> rator |> rand
@@ -4611,7 +4686,7 @@ fun translate_options options def =
       val (fname,ml_fname,def,th,pre) = hd results
     in
       if is_fun then let
-        val start_fun = start_timing "processing fun case"
+        val start_fun = start_timing (fn () => "processing fun case")
         val th = th |> INST [cl_env_tm |-> get_curr_env()]
         val n = ml_fname |> mlstringSyntax.mk_mlstring
         val lookup_var_assum = th |> hyp
@@ -4632,7 +4707,7 @@ fun translate_options options def =
         in allowing_rebind save_thm(fname ^ "_v_thm",v_thm) end
       else let (* not is_fun *)
 
-        val start_v = start_timing "processing val case"
+        val start_v = start_timing (fn () => "processing val case")
         val th = th |> INST [env_tm |-> get_curr_env()]
         val th = UNDISCH_ALL (clean_assumptions (D th))
         val curr_state = get_curr_state()
diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml
index 38e9ab404a..372fb7c498 100644
--- a/translator/ml_translatorScript.sml
+++ b/translator/ml_translatorScript.sml
@@ -760,7 +760,7 @@ Proof
 QED
 
 Theorem Eval_Implies:
-  Eval env x1 (BOOL b1) ==>
+  Eval env x1 (BOOL b1) /\
   Eval env x2 (BOOL b2) ==>
   Eval env (If x1 x2 True_ast) (BOOL (b1 ==> b2))
 Proof
@@ -775,7 +775,7 @@ Proof
 QED
 
 Theorem Eval_BOOL_EQ:
-  Eval env x1 (BOOL b1) ==>
+  Eval env x1 (BOOL b1) /\
   Eval env x2 (BOOL b2) ==>
   Eval env (App (Test Equal BoolT) [x1; x2]) (BOOL (b1 = b2))
 Proof
@@ -938,7 +938,7 @@ QED
 
 Theorem Eval_INT_ADD:
   ∀n1 n2.
-    Eval env x1 (INT n1) ⇒
+    Eval env x1 (INT n1) /\
     Eval env x2 (INT n2) ⇒
     Eval env (App (Arith Add IntT) [x1; x2]) (INT (n1 + n2))
 Proof
@@ -949,7 +949,7 @@ QED
 
 Theorem Eval_INT_SUB:
   ∀n1 n2.
-    Eval env x1 (INT n1) ⇒
+    Eval env x1 (INT n1) /\
     Eval env x2 (INT n2) ⇒
     Eval env (App (Arith Sub IntT) [x1; x2]) (INT (n1 - n2))
 Proof
@@ -960,7 +960,7 @@ QED
 
 Theorem Eval_INT_MULT:
   ∀n1 n2.
-    Eval env x1 (INT n1) ⇒
+    Eval env x1 (INT n1) /\
     Eval env x2 (INT n2) ⇒
     Eval env (App (Arith Mul IntT) [x1; x2]) (INT (n1 * n2))
 Proof
@@ -971,7 +971,7 @@ QED
 
 Theorem Eval_INT_DIV:
   ∀n1 n2.
-    Eval env x1 (INT n1) ⇒
+    Eval env x1 (INT n1) /\
     Eval env x2 (INT n2) ⇒
     PRECONDITION (n2 ≠ 0) ⇒
     Eval env (App (Arith Div IntT) [x1; x2]) (INT (n1 / n2))
@@ -983,7 +983,7 @@ QED
 
 Theorem Eval_INT_MOD:
   ∀n1 n2.
-    Eval env x1 (INT n1) ⇒
+    Eval env x1 (INT n1) /\
     Eval env x2 (INT n2) ⇒
     PRECONDITION (n2 ≠ 0) ⇒
     Eval env (App (Arith Mod IntT) [x1; x2]) (INT (n1 % n2))
@@ -995,7 +995,7 @@ QED
 
 Theorem Eval_INT_CMP[local]:
   ∀f n1 n2.
-    Eval env x1 (INT n1) ==>
+    Eval env x1 (INT n1) /\
     Eval env x2 (INT n2) ==>
     Eval env (App (Test (Compare f) IntT) [x1;x2]) (BOOL (int_cmp f n1 n2))
 Proof
@@ -1010,7 +1010,7 @@ Theorem Eval_INT_GREATER    = Eval_INT_CMP |> Q.SPEC ‘Gt’  |> SRULE [int_cmp
 Theorem Eval_INT_GREATER_EQ = Eval_INT_CMP |> Q.SPEC ‘Geq’ |> SRULE [int_cmp_def];
 
 Theorem Eval_INT_EQ:
-  Eval env x1 (INT i1) ==>
+  Eval env x1 (INT i1) /\
   Eval env x2 (INT i2) ==>
   Eval env (App (Test Equal IntT) [x1; x2]) (BOOL (i1 = i2))
 Proof
@@ -1022,14 +1022,13 @@ Proof
 QED
 
 Theorem Eval_NUM_EQ:
-  Eval env x1 (NUM n1) ==>
+  Eval env x1 (NUM n1) /\
   Eval env x2 (NUM n2) ==>
   Eval env (App (Test Equal IntT) [x1; x2]) (BOOL (n1 = n2))
 Proof
   rewrite_tac [NUM_def]
-  \\ strip_tac \\ drule Eval_INT_EQ
-  \\ rpt strip_tac
-  \\ first_x_assum dxrule \\ gvs []
+  \\ strip_tac \\ rev_dxrule_all Eval_INT_EQ
+  \\ simp []
 QED
 
 Theorem Eval_Num:
@@ -1043,11 +1042,11 @@ QED
 local
 
 val th0 = Q.SPEC `0` Eval_Val_INT
-val th_sub = MATCH_MP (MATCH_MP Eval_INT_SUB (Q.SPEC `0` Eval_Val_INT))
-            (ASSUME ``Eval env (Var (Short «k»)) (INT k)``)
+val th_sub = MATCH_MP Eval_INT_SUB (CONJ (Q.SPEC `0` Eval_Val_INT)
+            (ASSUME ``Eval env (Var (Short «k»)) (INT k)``))
 val th1 = ASSUME ``Eval env (Var (Short «k»)) (INT k)``
 val th2 = Eval_INT_LESS  |> Q.SPECL [`k`,`0`]
-          |> (fn th => MATCH_MP th th1) |> (fn th => MATCH_MP th th0)
+          |> (fn th => MATCH_MP th (CONJ th1 th0))
 val th = MATCH_MP Eval_If (LIST_CONJ (map (DISCH T) [th2,th_sub,th1]))
          |> REWRITE_RULE [CONTAINER_def]
 val code =
@@ -1126,8 +1125,7 @@ Theorem Eval_NUM_SUB =
   |> UNDISCH_ALL |> DISCH ``PRECONDITION ((m:num) <= n)``
   |> SIMP_RULE std_ss [GSYM NUM_def,INT_SUB,PRECONDITION_def]
   |> CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM PRECONDITION_def]))
-  |> DISCH ``Eval env x2 (INT (&m))``
-  |> DISCH ``Eval env x1 (INT (&n))``
+  |> DISCH ``Eval env x1 (INT (&n)) /\ Eval env x2 (INT (&m))``
   |> SIMP_RULE std_ss [GSYM NUM_def]
 
 Theorem Eval_NUM_ADD =
@@ -1143,8 +1141,7 @@ Theorem Eval_NUM_DIV =
   |> UNDISCH_ALL |> DISCH ``PRECONDITION (&n2 <> 0:int)``
   |> SIMP_RULE std_ss [GSYM NUM_def,INT_DIV,PRECONDITION_def,INT_INJ]
   |> CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM PRECONDITION_def]))
-  |> DISCH ``Eval env x2 (INT (&n2))``
-  |> DISCH ``Eval env x1 (INT (&n1))``
+  |> DISCH ``Eval env x1 (INT (&n1)) /\ Eval env x2 (INT (&n2))``
   |> SIMP_RULE std_ss [GSYM NUM_def,INT_DIV]
 
 Theorem Eval_NUM_MOD =
@@ -1152,20 +1149,15 @@ Theorem Eval_NUM_MOD =
   |> UNDISCH_ALL |> DISCH ``PRECONDITION (&n2 <> 0:int)``
   |> SIMP_RULE std_ss [GSYM NUM_def,INT_MOD,PRECONDITION_def,INT_INJ]
   |> CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM PRECONDITION_def]))
-  |> DISCH ``Eval env x2 (INT (&n2))``
-  |> DISCH ``Eval env x1 (INT (&n1))``
+  |> DISCH ``Eval env x1 (INT (&n1)) /\ Eval env x2 (INT (&n2))``
   |> SIMP_RULE std_ss [GSYM NUM_def,INT_MOD]
 
-val Eval_NUM_MULT =
-  Eval_INT_MULT |> Q.SPECL [`&n1`,`&n2`]
-  |> REWRITE_RULE [GSYM NUM_def,INT_MUL]
-
 local
 
 val th0 = Q.SPEC `0` Eval_Val_INT
 val th1 = ASSUME ``Eval env (Var (Short «k»)) (INT k)``
 val th2 = Eval_INT_LESS  |> Q.SPECL [`k`,`0`]
-          |> (fn th => MATCH_MP th th1) |> (fn th => MATCH_MP th th0)
+          |> (fn th => MATCH_MP th (CONJ th1 th0))
 val th = MATCH_MP Eval_If (LIST_CONJ (map (DISCH T) [th2,th0,th1]))
          |> REWRITE_RULE [CONTAINER_def]
 val code =
@@ -1180,7 +1172,7 @@ Definition sub_check_def:
 End
 
 Theorem Eval_NUM_SUB_check:
-  Eval env x1 (NUM m) ==>
+  Eval env x1 (NUM m) /\
   Eval env x2 (NUM n) ==>
   Eval env ^code (NUM (sub_check m n))
 Proof
@@ -1199,7 +1191,7 @@ Proof
 QED
 
 Theorem Eval_NUM_SUB_check':
-  Eval env x1 (NUM m) ==>
+  Eval env x1 (NUM m) /\
   Eval env x2 (NUM n) ==>
   Eval env ^code (NUM (m - n))
 Proof
@@ -1772,8 +1764,8 @@ End
 
 Theorem Eval_FLOAT_FMA:
   ∀f1 f2 f3.
-    Eval env x2 (FLOAT64 f2) ⇒
-    Eval env x3 (FLOAT64 f3) ⇒
+    Eval env x2 (FLOAT64 f2) /\
+    Eval env x3 (FLOAT64 f3) /\
     Eval env x1 (FLOAT64 f1) ⇒
     Eval env
          (App (Arith FMA Float64T) [x1; x2; x3])
@@ -1848,7 +1840,7 @@ QED
 
 Theorem Eval_FLOAT_ADD:
   ∀f1 f2.
-    Eval env x1 (FLOAT64 f1) ⇒
+    Eval env x1 (FLOAT64 f1) /\
     Eval env x2 (FLOAT64 f2) ⇒
     Eval env (App (Arith Add Float64T) [x1; x2]) (FLOAT64 (float64_add f1 f2))
 Proof
@@ -1861,7 +1853,7 @@ QED
 
 Theorem Eval_FLOAT_SUB:
   ∀f1 f2.
-    Eval env x1 (FLOAT64 f1) ⇒
+    Eval env x1 (FLOAT64 f1) /\
     Eval env x2 (FLOAT64 f2) ⇒
     Eval env (App (Arith Sub Float64T) [x1; x2]) (FLOAT64 (float64_sub f1 f2))
 Proof
@@ -1874,7 +1866,7 @@ QED
 
 Theorem Eval_FLOAT_MULT:
   ∀f1 f2.
-    Eval env x1 (FLOAT64 f1) ⇒
+    Eval env x1 (FLOAT64 f1) /\
     Eval env x2 (FLOAT64 f2) ⇒
     Eval env (App (Arith Mul Float64T) [x1; x2]) (FLOAT64 (float64_mul f1 f2))
 Proof
@@ -1887,7 +1879,7 @@ QED
 
 Theorem Eval_FLOAT_DIV:
   ∀f1 f2.
-    Eval env x1 (FLOAT64 f1) ⇒
+    Eval env x1 (FLOAT64 f1) /\
     Eval env x2 (FLOAT64 f2) ⇒
     Eval env (App (Arith Div Float64T) [x1; x2]) (FLOAT64 (float64_div f1 f2))
 Proof
@@ -1961,7 +1953,7 @@ QED
 
 Theorem Eval_FP_cmp[local]:
   !cmp f1 f2.
-    Eval env x1 (FLOAT64 f1) ==>
+    Eval env x1 (FLOAT64 f1) /\
     Eval env x2 (FLOAT64 f2) ==>
     Eval env (App (Test (Compare cmp) Float64T) [x1;x2]) (BOOL (lift_fp_cmp cmp f1 f2))
 Proof
@@ -1990,7 +1982,7 @@ in
 end;
 
 Theorem Eval_FLOAT_EQ:
-  Eval env x1 (FLOAT64 f1) ==>
+  Eval env x1 (FLOAT64 f1) /\
   Eval env x2 (FLOAT64 f2) ==>
   Eval env (App (Test Equal Float64T) [x1;x2]) (BOOL (float64_equal f1 f2))
 Proof
@@ -2230,7 +2222,7 @@ Proof
 QED
 
 Theorem Eval_char_lt:
-  Eval env x1 (CHAR c1) ==>
+  Eval env x1 (CHAR c1) /\
   Eval env x2 (CHAR c2) ==>
   Eval env (App (Test (Compare Lt) CharT) [x1;x2]) (BOOL (c1 < c2))
 Proof
@@ -2241,7 +2233,7 @@ Proof
 QED
 
 Theorem Eval_char_le:
-  Eval env x1 (CHAR c1) ==>
+  Eval env x1 (CHAR c1) /\
   Eval env x2 (CHAR c2) ==>
   Eval env (App (Test (Compare Leq) CharT) [x1;x2]) (BOOL (c1 <= c2))
 Proof
@@ -2252,19 +2244,17 @@ Proof
 QED
 
 Theorem Eval_char_gt = Eval_char_lt
-  |> REWRITE_RULE [GSYM char_gt_def,char_lt_def,GSYM GREATER_DEF,AND_IMP_INTRO]
+  |> REWRITE_RULE [GSYM char_gt_def,char_lt_def,GSYM GREATER_DEF]
   |> Q.INST [‘x1’|->‘x2’,‘x2’|->‘x1’,‘c1’|->‘c2’,‘c2’|->‘c1’]
-  |> ONCE_REWRITE_RULE [CONJ_COMM]
-  |> REWRITE_RULE [GSYM AND_IMP_INTRO];
+  |> ONCE_REWRITE_RULE [CONJ_COMM];
 
 Theorem Eval_char_ge = Eval_char_le
-  |> REWRITE_RULE [GSYM char_ge_def,char_le_def,GSYM GREATER_EQ,AND_IMP_INTRO]
+  |> REWRITE_RULE [GSYM char_ge_def,char_le_def,GSYM GREATER_EQ]
   |> Q.INST [‘x1’|->‘x2’,‘x2’|->‘x1’,‘c1’|->‘c2’,‘c2’|->‘c1’]
-  |> ONCE_REWRITE_RULE [CONJ_COMM]
-  |> REWRITE_RULE [GSYM AND_IMP_INTRO];
+  |> ONCE_REWRITE_RULE [CONJ_COMM];
 
 Theorem Eval_char_eq:
-  Eval env x1 (CHAR c1) ==>
+  Eval env x1 (CHAR c1) /\
   Eval env x2 (CHAR c2) ==>
   Eval env (App (Test Equal CharT) [x1; x2]) (BOOL (c1 = c2))
 Proof
@@ -2329,8 +2319,7 @@ Proof
 QED
 
 Theorem Eval_strsub:
-   !env x1 x2 s n.
-      Eval env x1 (STRING_TYPE s) ==>
+      Eval env x1 (STRING_TYPE s) /\
       Eval env x2 (NUM n) ==>
       n < strlen s ==>
       Eval env (App Strsub [x1; x2]) (CHAR (strsub s n))
@@ -2361,8 +2350,8 @@ QED
 
 Theorem Eval_substring:
    ∀env x1 x2 x3 len off st.
-    Eval env x1 (STRING_TYPE st) ==>
-    Eval env x2 (NUM off) ==>
+    Eval env x1 (STRING_TYPE st) /\ 
+    Eval env x2 (NUM off) /\ 
     Eval env x3 (NUM len) ==>
       off + len <= strlen st ==>
     Eval env (App CopyStrStr [x1; x2; x3]) (STRING_TYPE (substring st off len))
@@ -2397,7 +2386,7 @@ val str_cmp_tac =
   \\ fs [ctor_same_type_def,same_type_def,BOOL_def];
 
 Theorem Eval_str_eq:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test Equal StrT) [x1; x2]) (BOOL (s1 = s2))
 Proof
@@ -2405,7 +2394,7 @@ Proof
 QED
 
 Theorem Eval_mlstring_lt:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (Compare Lt) StrT) [x1; x2]) (BOOL (mlstring_lt s1 s2))
 Proof
@@ -2413,7 +2402,7 @@ Proof
 QED
 
 Theorem Eval_mlstring_le:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (Compare Leq) StrT) [x1; x2]) (BOOL (mlstring_le s1 s2))
 Proof
@@ -2421,7 +2410,7 @@ Proof
 QED
 
 Theorem Eval_mlstring_gt:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (Compare Gt) StrT) [x1; x2]) (BOOL (mlstring_gt s1 s2))
 Proof
@@ -2429,7 +2418,7 @@ Proof
 QED
 
 Theorem Eval_mlstring_ge:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (Compare Geq) StrT) [x1; x2]) (BOOL (mlstring_ge s1 s2))
 Proof
@@ -2437,7 +2426,7 @@ Proof
 QED
 
 Theorem Eval_fast_lt:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (AltCompare Lt) StrT) [x1; x2]) (BOOL (fast_lt s1 s2))
 Proof
@@ -2445,7 +2434,7 @@ Proof
 QED
 
 Theorem Eval_fast_le:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (AltCompare Leq) StrT) [x1; x2]) (BOOL (fast_le s1 s2))
 Proof
@@ -2453,7 +2442,7 @@ Proof
 QED
 
 Theorem Eval_fast_gt:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (AltCompare Gt) StrT) [x1; x2]) (BOOL (fast_gt s1 s2))
 Proof
@@ -2461,7 +2450,7 @@ Proof
 QED
 
 Theorem Eval_fast_ge:
-  Eval env x1 (STRING_TYPE s1) ==>
+  Eval env x1 (STRING_TYPE s1) /\
   Eval env x2 (STRING_TYPE s2) ==>
   Eval env (App (Test (AltCompare Geq) StrT) [x1; x2]) (BOOL (fast_ge s1 s2))
 Proof
@@ -2513,7 +2502,7 @@ QED
 
 Theorem Eval_HOL_STRING_EL:
    !env x1 x2 s n.
-      Eval env x2 (NUM n) ==>
+      Eval env x2 (NUM n) /\
       Eval env x1 (HOL_STRING_TYPE s) ==>
       n < LENGTH s ==>
       Eval env (App Strsub [x1; x2]) (CHAR (EL n s))
@@ -2536,7 +2525,7 @@ QED
 
 Theorem Eval_HOL_STRING_APPEND:
    !env x1 x2 s1 s2 n.
-      Eval env x1 (HOL_STRING_TYPE s1) ==>
+      Eval env x1 (HOL_STRING_TYPE s1) /\
       Eval env x2 (HOL_STRING_TYPE s2) ==>
       lookup_cons (Short «::») env = SOME (2,TypeStamp «::» 1) /\
       lookup_cons (Short «[]») env = SOME (0,TypeStamp «[]» 1) ==>
@@ -2564,8 +2553,7 @@ Proof
 QED
 
 Theorem Eval_HOL_STRING_CONS:
-   !env x1 x2 c s n.
-      Eval env x1 (CHAR c) ==>
+      Eval env x1 (CHAR c) /\
       Eval env x2 (HOL_STRING_TYPE s) ==>
       lookup_cons (Short «::») env = SOME (2,TypeStamp «::» 1) /\
       lookup_cons (Short «[]») env = SOME (0,TypeStamp «[]» 1) ==>
@@ -2655,8 +2643,7 @@ Proof
 QED
 
 Theorem Eval_sub:
-  !env x1 x2 a n v.
-     Eval env x1 (VECTOR_TYPE a v) ==>
+     Eval env x1 (VECTOR_TYPE a v) /\
      Eval env x2 (NUM n) ==>
      n < length v ==>
      Eval env (App Vsub [x1; x2]) (a (sub v n))
@@ -2669,8 +2656,7 @@ Proof
 QED
 
 Theorem Eval_sub_unsafe:
-  !env x1 x2 a n v.
-     Eval env x1 (VECTOR_TYPE a v) ==>
+     Eval env x1 (VECTOR_TYPE a v) /\
      Eval env x2 (NUM n) ==>
      n < length v ==>
      Eval env (App Vsub_unsafe [x1; x2]) (a (sub_unsafe v n))
@@ -2732,8 +2718,7 @@ Proof
 QED
 
 Theorem Eval_ListAppend:
-   !env x1 x2 a l1 l2.
-     Eval env x2 (LIST_TYPE a l1) ==>
+     Eval env x2 (LIST_TYPE a l1) /\
      Eval env x1 (LIST_TYPE a l2) ==>
      Eval env (App ListAppend [x2;x1]) (LIST_TYPE a (l1 ++ l2))
 Proof
@@ -2759,7 +2744,7 @@ Definition force_unit_type_def[simp,compute]:
 End
 
 Theorem Eval_force_unit_type:
-    Eval env x1 (UNIT_TYPE u) ==>
+    Eval env x1 (UNIT_TYPE u) /\
     Eval env x2 ((a:'a -> v -> bool) y) ==>
     Eval env (Mat x1 [(Pcon NONE [], x2)]) (a (force_unit_type u y))
 Proof
@@ -2783,7 +2768,7 @@ Definition force_gc_to_run_def:
 End
 
 Theorem Eval_force_gc_to_run:
-    Eval env x1 (INT i1) ==>
+    Eval env x1 (INT i1) /\
     Eval env x2 (INT i2) ==>
     Eval env (App ConfigGC [x1; x2]) (UNIT_TYPE (force_gc_to_run i1 i2))
 Proof
@@ -2831,7 +2816,7 @@ Definition pure_seq_def:
 End
 
 Theorem Eval_pure_seq:
-   Eval env x (a a1) ==>
+   Eval env x (a a1) /\
    Eval env y (b b1) ==>
    Eval env (Let NONE x y) (b (pure_seq a1 b1))
 Proof
@@ -3277,17 +3262,6 @@ Proof
   Cases_on `b1` \\ Cases_on `x1` \\ Cases_on `x2` \\ Cases_on `y` \\ EVAL_TAC
 QED
 
-Theorem IMP_EQ_F:
-  ~b ==> (b = F)
-Proof
-REWRITE_TAC []
-QED
-Theorem IMP_EQ_T:
-  b ==> (b = T)
-Proof
-REWRITE_TAC []
-QED
-
 Theorem IF_TAKEN:
    !b x y. b ==> ((if b then x else y) = x:'unlikely)
 Proof
diff --git a/translator/ml_translatorSyntax.sig b/translator/ml_translatorSyntax.sig
index da3182036f..ee629e2991 100644
--- a/translator/ml_translatorSyntax.sig
+++ b/translator/ml_translatorSyntax.sig
@@ -46,15 +46,16 @@ sig
   val TRUE  : term
   val FALSE : term
 
-  val BOOL        : term
-  val WORD        : term
-  val FLOAT64     : term
-  val NUM         : term
-  val INT         : term
-  val CHAR        : term
-  val STRING_TYPE : term
-  val UNIT_TYPE   : term
-  val LIST_TYPE   : term
+  val BOOL            : term
+  val WORD            : term
+  val FLOAT64         : term
+  val NUM             : term
+  val INT             : term
+  val CHAR            : term
+  val STRING_TYPE     : term
+  val HOL_STRING_TYPE : term
+  val UNIT_TYPE       : term
+  val LIST_TYPE       : term
 
   val DUMMY_TYPE_REP_v  : term
 
diff --git a/translator/ml_translatorSyntax.sml b/translator/ml_translatorSyntax.sml
index 1caf5bdaff..72fda490b6 100644
--- a/translator/ml_translatorSyntax.sml
+++ b/translator/ml_translatorSyntax.sml
@@ -17,14 +17,15 @@ val (CONTAINER,mk_CONTAINER,dest_CONTAINER,is_CONTAINER) = monop "CONTAINER";
 val (PRECONDITION,mk_PRECONDITION,dest_PRECONDITION,is_PRECONDITION) = monop "PRECONDITION";
 val (IsTypeRep,mk_IsTypeRep,dest_IsTypeRep,is_IsTypeRep) = binop "IsTypeRep";
 
-val BOOL        = prim_mk_const{Thy="ml_translator",Name="BOOL"}
-val WORD        = prim_mk_const{Thy="ml_translator",Name="WORD"}
-val FLOAT64     = prim_mk_const{Thy="ml_translator",Name="FLOAT64"}
-val NUM         = prim_mk_const{Thy="ml_translator",Name="NUM"}
-val INT         = prim_mk_const{Thy="ml_translator",Name="INT"}
-val CHAR        = prim_mk_const{Thy="ml_translator",Name="CHAR"}
-val STRING_TYPE = prim_mk_const{Thy="ml_translator",Name="STRING_TYPE"}
-val UNIT_TYPE   = prim_mk_const{Thy="ml_translator",Name="UNIT_TYPE"}
+val BOOL            = prim_mk_const{Thy="ml_translator",Name="BOOL"}
+val WORD            = prim_mk_const{Thy="ml_translator",Name="WORD"}
+val FLOAT64         = prim_mk_const{Thy="ml_translator",Name="FLOAT64"}
+val NUM             = prim_mk_const{Thy="ml_translator",Name="NUM"}
+val INT             = prim_mk_const{Thy="ml_translator",Name="INT"}
+val CHAR            = prim_mk_const{Thy="ml_translator",Name="CHAR"}
+val STRING_TYPE     = prim_mk_const{Thy="ml_translator",Name="STRING_TYPE"}
+val HOL_STRING_TYPE = prim_mk_const{Thy="ml_translator",Name="HOL_STRING_TYPE"}
+val UNIT_TYPE       = prim_mk_const{Thy="ml_translator",Name="UNIT_TYPE"}
 
 val DUMMY_TYPE_REP_v = prim_mk_const{Thy="ml_translator",Name="DUMMY_TYPE_REP_v"}
 
diff --git a/translator/ml_translatorTrace.sml b/translator/ml_translatorTrace.sml
new file mode 100644
index 0000000000..1a0c59357c
--- /dev/null
+++ b/translator/ml_translatorTrace.sml
@@ -0,0 +1,44 @@
+structure ml_translatorTrace (* TODO :> ml_translatorTrace *) =
+struct
+
+open Feedback boolSyntax Abbrev;
+
+val print_term = Lib.say o Parse.term_to_string
+val print_thm = Parse.print_thm
+val concl = Thm.concl
+val say = Lib.say
+
+   (* ---------------------------------------------------------------------
+    * Tracing utilities
+    * ---------------------------------------------------------------------*)
+    (* TODO add more utilities *)
+    datatype action =
+             LZ_TEXT of unit -> string
+           | TEXT of string;
+
+   val trace_hook : (int * action) Listener.t = Listener.new_listener()
+   fun trace x = ignore (Listener.call_listener trace_hook x)
+
+val trace_level = ref 0;
+val _ = Feedback.register_trace("ml_translator", trace_level, 7);
+
+fun tty_trace (LZ_TEXT fs) = (say "  "; say (fs ()); say "\n")
+  | tty_trace (TEXT s) = (say "  "; say s; say "\n");
+
+(* hol_clock is sometimes a small amount of time in the future under Poly/ML,
+   presumably a consequence of being stored in a heap.
+*)
+fun fudge t = Time.+(t, Time.fromSeconds 10)
+
+val _ = Listener.add_listener trace_hook
+        ("default",
+         (fn (n,a) => if (n <= !trace_level) then
+                        (say "[";
+                         say ((Arbnum.toString o #usec o Portable.dest_time o
+                               fudge)
+                                (#usr (Timer.checkCPUTimer Globals.hol_clock)));
+                         say "]: ";
+                         tty_trace a)
+                      else ()))
+
+end (* struct *)
diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml
index 5ba8548243..c4751f1e37 100644
--- a/translator/ml_translator_testScript.sml
+++ b/translator/ml_translator_testScript.sml
@@ -21,11 +21,12 @@ val _ = register_type “:a_ty”;
 val ty = “:a_ty”;
 
 Definition dest_A2_def:
-  dest_A2 (A2 a) = SOME a ∧
+  dest_A2 (A2 a) = (if a = A1 then NONE else SOME a) ∧
   dest_A2 _ = NONE
 End
 
 val r = translate dest_A2_def;
+val _ = (List.null $ Thm.hyp r) orelse fail()
 
 Datatype:
   tyAST = tyOp string (tyAST list)
diff --git a/translator/monadic/ml_monad_translatorLib.sml b/translator/monadic/ml_monad_translatorLib.sml
index 52c07bfa9d..3030df8209 100644
--- a/translator/monadic/ml_monad_translatorLib.sml
+++ b/translator/monadic/ml_monad_translatorLib.sml
@@ -1789,7 +1789,7 @@ fun prove_EvalMPatBind goal = let
   val all_assums = append vs assums
   fun delete_assum tm =
     if tmem tm (all_assums) then
-      MATCH_MP ml_monad_translatorTheory.IMP_EQ_T (ASSUME tm)
+      EQT_INTRO (ASSUME tm)
     else NO_CONV tm
   val th = CONV_RULE ((RATOR_CONV) (DEPTH_CONV delete_assum)) th
   val th = CONV_RULE ((RATOR_CONV) (SIMP_CONV bool_ss [])) th
@@ -2088,7 +2088,7 @@ and m2deep_normal_fun_app tm = let
     val assums = find_terms is_var_lookup_eqtype_assum (concl thx)
     fun delete_assums tm =
       if tmem tm assums then
-        MATCH_MP ml_monad_translatorTheory.IMP_EQ_T (ASSUME tm)
+        EQT_INTRO (ASSUME tm)
       else NO_CONV tm
     val thx = CONV_RULE ((RATOR_CONV) (DEPTH_CONV delete_assums)) thx
     val thx = CONV_RULE ((RATOR_CONV o RAND_CONV)
@@ -3224,7 +3224,7 @@ fun update_local_precondition new_pre = let
         val (new_pre,th1) =
           (if is_imp (concl (SPEC_ALL new_pre))
            then (* case: new_pre is an induction theorem *)
-             (((MATCH_MP IMP_EQ_T (MP (disch_asms new_pre) TRUTH)
+             (((EQT_INTRO (MP (disch_asms new_pre) TRUTH)
                handle HOL_ERR _ => new_pre)
                |> PURE_REWRITE_RULE [GSYM CONJ_ASSOC]),
               PURE_REWRITE_RULE [GSYM CONJ_ASSOC] th1)
diff --git a/translator/monadic/ml_monad_translatorScript.sml b/translator/monadic/ml_monad_translatorScript.sml
index d90d34c099..43b3b78e92 100644
--- a/translator/monadic/ml_monad_translatorScript.sml
+++ b/translator/monadic/ml_monad_translatorScript.sml
@@ -3561,12 +3561,6 @@ Proof
 SIMP_TAC std_ss []
 QED
 
-Theorem IMP_EQ_T:
-  a ==> (a <=> T)
-Proof
-fs []
-QED
-
 Theorem BETA_PAIR_THM:
   (\(x, y). f x y) (x, y) = (\x y. f x y) x y
 Proof