diff --git a/translator/monadic/ml_monadStoreLib.sml b/translator/monadic/ml_monadStoreLib.sml
index d8817b73bd..0c48bc85c2 100644
--- a/translator/monadic/ml_monadStoreLib.sml
+++ b/translator/monadic/ml_monadStoreLib.sml
@@ -50,32 +50,38 @@ local
   end
   open Parse
   (* Information about the subscript exceptions *)
-  val Conv_Subscript = EVAL ``sub_exn_v`` |> concl |> rand
+  val Conv_Subscript = EVAL semanticPrimitivesSyntax.sub_exn_v |> concl |> rand
   (* val Stamp_Subscript = Conv_Subscript |> rator |> rand |> rand *)
 in
 
+(* Sidestep setting up "syntax" libraries, fetch const from def. *)
+fun left_const thm = concl thm
+    |> strip_conj |> hd |> strip_forall |> snd |> lhs
+    |> strip_comb |> fst
+
 (* Constants *)
-val hprop_ty = “:hprop”
-val v_ty = “:v”
-val ffi_state_ty = “:'ffi semanticPrimitives$state”
-val ffi_ffi_proj_ty = “:'ffi ffi_proj”
-val lookup_ret_ty = “:num # stamp”
+val hprop_ty = cfHeapsBaseSyntax.hprop_ty
+val v_ty = semanticPrimitivesSyntax.v_ty
+val ffi_var = mk_vartype "'ffi"
+val ffi_state_ty = semanticPrimitivesSyntax.state_ty |> type_subst [alpha |-> ffi_var]
+val ffi_ffi_proj_ty = cfHeapsBaseSyntax.mk_ffi_proj_ty ffi_var
+val lookup_ret_ty = pairSyntax.mk_prod(numSyntax.num, semanticPrimitivesSyntax.stamp_ty)
 
 val TRUE = boolSyntax.T
-val emp_const = “emp : hprop”
-val APPEND_const = “APPEND : α list -> α list -> α list”
-val CONS_const = “CONS : α -> α list -> α list”
-val REF_const = “REF”
-val RARRAY_const = “RARRAY”
-val ARRAY_const = “ARRAY”
-val SOME_const = “SOME”
-val one_const = “1 : num”
-val cond_const = “set_sep$cond”
+val emp_const = cfHeapsBaseSyntax.emp_tm
+val APPEND_const = listSyntax.append_tm
+val CONS_const = listSyntax.cons_tm
+val REF_const = cfHeapsBaseTheory.REF_def |> left_const
+val RARRAY_const = ml_monad_translatorBaseTheory.RARRAY_def |> left_const
+val ARRAY_const = cfHeapsBaseTheory.ARRAY_def |> left_const
+val one_const = numSyntax.term_of_int 1
+val cond_const = set_sepTheory.cond_def |> left_const
 val get_refs_const = “λ(state : 'a semanticPrimitives$state). state.refs”
 val opref_expr = “λname. (App Opref [Var (Short name)])”
-val empty_v_list = “[] : v list”
-val empty_v_store = “[] : v store”
-val empty_alpha_list = “[] : α list”
+val empty_v_list = listSyntax.mk_list ([], v_ty)
+val empty_v_store = listSyntax.mk_list ([],
+    semanticPrimitivesSyntax.store_v_ty |> type_subst [alpha |-> v_ty])
+val empty_alpha_list = listSyntax.mk_list ([], alpha)
 val nsLookup_env_short_term = “λ(env : v sem_env) name. nsLookup env.v (Short name)”
 val Conv_Subscript = Conv_Subscript
 end (* local *)
@@ -105,7 +111,7 @@ fun mk_VALID_REFS_PRED H =
 
 fun mk_lookup_eq name env type_tm = let
     val lookup_tm = ISPECL [name, env] lookup_cons_def |> concl |> dest_eq |> fst
-    val some_tm = mk_comb (inst [alpha |-> lookup_ret_ty] SOME_const, mk_pair(one_const, type_tm))
+    val some_tm = optionSyntax.mk_some(mk_pair(one_const, type_tm))
 in mk_eq(lookup_tm, some_tm) end
 
 (******* COPY/PASTE from ml_monadProgScript.sml *****************************************)
@@ -418,8 +424,7 @@ fun create_store_X_hprop refs_manip_list
         val get_term = mk_comb (get_f, Term.inst ty_subst state_var) |>
                        BETA_CONV |> concl |> dest_eq |> snd
 
-        val hprop =
-          list_mk_ucomb(``RARRAY_REL``, [ref_inv, rarray_ref_loc, get_term])
+        val hprop = mk_RARRAY_REL ref_inv rarray_ref_loc get_term
       in
         hprop
       end
@@ -441,7 +446,7 @@ fun create_store_X_hprop refs_manip_list
         val get_term = mk_comb (get_f, Term.inst ty_subst state_var) |>
                        BETA_CONV |> concl |> dest_eq |> snd
 
-        val hprop = list_mk_ucomb(``ARRAY_REL``, [ref_inv, farray_loc, get_term])
+        val hprop = mk_ARRAY_REL ref_inv farray_loc get_term
       in
         hprop
       end
diff --git a/translator/monadic/ml_monad_translator_interfaceLib.sig b/translator/monadic/ml_monad_translator_interfaceLib.sig
index 7d9b8a6c03..5fe5af92df 100644
--- a/translator/monadic/ml_monad_translator_interfaceLib.sig
+++ b/translator/monadic/ml_monad_translator_interfaceLib.sig
@@ -47,6 +47,9 @@
 signature ml_monad_translator_interfaceLib =
 sig
 
+  (* Sets up monadic syntax, Less invasive than the full version. *)
+  val minimal_set_up_monadic_translator : unit -> unit
+
   val set_up_monadic_translator : unit -> unit
 
   type term = Term.term
diff --git a/translator/monadic/ml_monad_translator_interfaceLib.sml b/translator/monadic/ml_monad_translator_interfaceLib.sml
index c75a00dda8..c8642e5ee2 100644
--- a/translator/monadic/ml_monad_translator_interfaceLib.sml
+++ b/translator/monadic/ml_monad_translator_interfaceLib.sml
@@ -15,16 +15,29 @@ open preamble ml_monadBaseLib ml_monadStoreLib ml_monad_translatorLib
 
 ******************************************************************************)
 
-fun set_up_monadic_translator () = let
+(* Sidestep setting up "syntax" libraries, fetch const from def. *)
+fun left_const thm = concl thm
+    |> strip_conj |> hd |> strip_forall |> snd |> lhs
+    |> strip_comb |> fst
+
+fun minimal_set_up_monadic_translator () = let
   (* Add monadic syntax: do x <- f y; ... od *)
-  val _ = ParseExtras.temp_loose_equality();
   val _ = monadsyntax.temp_add_monadsyntax()
 
   (* Parser overloadings *)
-  val _ = Parse.temp_overload_on("monad_bind",``st_ex_bind``);
-  val _ = Parse.temp_overload_on("monad_unitbind",``st_ex_ignore_bind``);
-  val _ = Parse.temp_overload_on("monad_ignore_bind",``st_ex_ignore_bind``);
-  val _ = Parse.temp_overload_on("return",``st_ex_return``);
+  open ml_monadBaseTheory
+  val _ = Parse.temp_overload_on("monad_bind", left_const st_ex_bind_def);
+  val ign_c = left_const st_ex_ignore_bind_def;
+  val _ = Parse.temp_overload_on("monad_unitbind", ign_c);
+  val _ = Parse.temp_overload_on("monad_ignore_bind", ign_c);
+  val _ = Parse.temp_overload_on("return", left_const st_ex_return_def);
+in () end
+
+fun set_up_monadic_translator () = let
+  (* Take all steps taken by a previous version. *)
+  val _ = ParseExtras.temp_loose_equality();
+
+  val _ = minimal_set_up_monadic_translator();
 
   (* Hide "state" due to semanticPrimitives *)
   val _ = hide "state";
@@ -39,8 +52,7 @@ in () end
 
 ******************************************************************************)
 
-fun toUppers(str) = String.implode (map Char.toUpper (String.explode str));
-val unit_ty = type_of ``()``;
+val unit_ty = type_of (left_const oneTheory.one_DEF);
 
 
 datatype translator_mode = GLOBAL | LOCAL;
@@ -56,8 +68,6 @@ datatype translator_mode = GLOBAL | LOCAL;
 type state = {
   state_access_funs         : (string * thm * thm) list ref,
                                 (* (name, get, set) *)
-  store_invariant_name      : string ref,
-  store_exn_invariant_name  : string ref,
   exn_type_def              : thm ref,
   additional_type_theories  : string list ref,
   hprop_field_names         : (term * string) list ref,
@@ -71,8 +81,6 @@ type state = {
 (* Initial internal state *)
 val internal_state : state = {
   state_access_funs        = ref [],
-  store_invariant_name     = ref "STATE_STORE",
-  store_exn_invariant_name = ref "STATE_EXN",
   exn_type_def             = ref ml_translatorTheory.UNIT_TYPE_def,
   additional_type_theories = ref [],
   hprop_field_names        = ref [],
@@ -139,27 +147,27 @@ fun with_state state_type (translator_config : config) =
   let val accessors = define_monad_access_funs state_type
   in
     #state_type internal_state := state_type;
-    #store_invariant_name internal_state :=
-      (state_type |> dest_type |> fst |> toUppers);
     #state_access_funs internal_state := accessors;
     translator_config
   end;
 
+(* This hack also used in ml_translatorLib. *)
+fun guess_const_def tm = let
+    val stuff = dest_thy_const tm
+  in DB.fetch (#Thy stuff) (#Name stuff ^ "_def") end
+
 (*
  *  Register the exception type and return the type definition
  *)
 fun register_exception_type exn_type =
-  let val exn_name = (exn_type |> dest_type |> fst |> toUppers)
-      val exn_type_def_name = exn_name ^ "_TYPE_def"
-  in (
+  (
     register_type ``:unit``;
     register_type ``:'a # 'b``;
     register_type ``:'a list``;
     register_type ``:'a option``;
     register_exn_type exn_type;
-    #store_exn_invariant_name internal_state := exn_name;
-    theorem exn_type_def_name
-  ) end;
+    guess_const_def (get_type_inv exn_type)
+  );
 
 (*
  *  Set the exception type, and get monadic exception functions
@@ -344,7 +352,7 @@ fun extract_farrays_manip_funs (name, init, get, set, len, sub, upd) =
 local
 
   val IMP_STAR_GC = Q.prove(
-      `(STAR a x) s ∧ (y = GC) ⇒ (STAR a y) s`,
+      `(STAR a x) s ∧ (y = cfHeapsBase$GC) ⇒ (STAR a y) s`,
       fs [set_sepTheory.STAR_def] >>
       rw [] >> asm_exists_tac >> fs [] >>
       EVAL_TAC >>
@@ -356,11 +364,9 @@ local
 in
 
   fun add_field_access_patterns (hprop_comb, field_name) = let
-    val store_inv_name = ( !(#store_invariant_name internal_state) )
     val state_ty = ( !(#state_type internal_state) )
-    val state_predicate =
-      if state_ty = unit_ty then ``UNIT_TYPE``
-      else Term [QUOTE store_inv_name]
+    val state_predicate = get_type_inv state_ty
+    val state_predicate_def = guess_const_def state_predicate
     val field = Term [QUOTE field_name]
     val st_field = Term [QUOTE "st.", QUOTE field_name]
 
@@ -382,7 +388,7 @@ in
         impl_tac
         >- (
           fs [ml_monad_translatorBaseTheory.REFS_PRED_def] >>
-          fs [fetch "-" (store_inv_name ^ "_def")] >>
+          fs [state_predicate_def] >>
           qabbrev_tac `a = ^hprop_comb ^st_field` >>
           qabbrev_tac `b = GC` >>
           fs [AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM] >>
@@ -397,18 +403,15 @@ in
         Cases_on `f ^st_field` >> fs [] >>
         EVERY_CASE_TAC >>
         rveq >> fs [] >>
-        fs [fetch "-" (store_inv_name ^ "_def")] >>
+        fs [state_predicate_def] >>
         fs [ml_monadBaseTheory.liftM_def] >>
         rw [] >>
         rfs[] >>
         fs[HPROP_COMB_STAR_COMM, set_sepTheory.STAR_ASSOC] >>
         metis_tac[set_sepTheory.STAR_ASSOC]
       )
-    val state_exn_name = ( !(#store_exn_invariant_name internal_state) )
     val state_exn_ty = ( !(#exn_type internal_state) )
-    val state_exn_predicate =
-      if state_exn_ty = unit_ty then ``UNIT_TYPE``
-      else Term [QUOTE state_exn_name, QUOTE "_TYPE"]
+    val state_exn_predicate = get_type_inv state_exn_ty
 
     val access_thm_list = mapfilter
       (fn ((_, name), (thm, Thm, _)) => (name^"_"^field_name, thm)
@@ -464,7 +467,7 @@ fun start_translation (translator_config : config) =
           ((!(#refs                     c) ) |> map from_named_tuple_refs)
           ((!(#resizeable_arrays        c) ) |> map from_named_tuple_rarray)
           ((!(#fixed_arrays             c) ) |> map from_named_tuple_farray)
-          ( !(#store_invariant_name     s) )
+          ((!(#state_type               c) ) |> dest_type |> fst |> (fn s => s^"_STORE_INV"))
           ( !(#state_type               c) )
           ( !(#exn_type_def             s) )
           ((!(#exn_access_funs          c) ) |> map from_named_tuple_exn)
@@ -485,7 +488,7 @@ fun start_translation (translator_config : config) =
                                                 map extract_rarrays_manip_funs)
           ((!(#fixed_arrays             c) ) |> map from_named_tuple_farray |>
                                                 map extract_farrays_manip_funs)
-          ( !(#store_invariant_name     s) )
+          ((!(#state_type               c) ) |> dest_type |> fst |> (fn s => s^"_STORE_INV"))
           ( !(#state_type               c) )
           ( !(#exn_type_def             s) )
           ((!(#exn_access_funs          c) ) |> map from_named_tuple_exn)