Update HOL4 snapshot

22 files changed, 329 insertions, 330 deletions

diff --git a/snapshots/hol4/lem/hol-lib/lem_assert_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_assert_extraScript.sml
index 7ef74237..79d5eda7 100644
--- a/snapshots/hol4/lem/hol-lib/lem_assert_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_assert_extraScript.sml
@@ -35,8 +35,8 @@ val _ = Define `
 
 (*val ensure : bool -> string -> unit*)
 val _ = Define `
- ((ensure:bool -> string -> unit) test msg=  
- (if test then
+ ((ensure:bool -> string -> unit) test msg=
+   (if test then
     () 
   else
     failwith msg))`;
diff --git a/snapshots/hol4/lem/hol-lib/lem_basic_classesScript.sml b/snapshots/hol4/lem/hol-lib/lem_basic_classesScript.sml
index eba5f169..4788ee10 100644
--- a/snapshots/hol4/lem/hol-lib/lem_basic_classesScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_basic_classesScript.sml
@@ -1,6 +1,6 @@
 (*Generated by Lem from basic_classes.lem.*)
 open HolKernel Parse boolLib bossLib;
-open lem_boolTheory;
+open lem_boolTheory ternaryComparisonsTheory;
 
 val _ = numLib.prefer_num();
 
@@ -15,6 +15,7 @@ val _ = new_theory "lem_basic_classes"
 (*open import Bool*) 
 
 (*open import {coq} `Coq.Strings.Ascii`*)
+(*open import {hol} `ternaryComparisonsTheory`*)
 
 (* ========================================================================== *)
 (* Equality                                                                   *)
@@ -65,26 +66,24 @@ lemma eq_equiv: ((forall x. (x = x)) &&
 (* ========================================================================== *)
 
 (* The type-class Ord represents total orders (also called linear orders) *)
-val _ = Hol_datatype `
- ordering = LT | EQ | GT`;
-
+(*type ordering = LT | EQ | GT*)
 
 val _ = Define `
- ((orderingIsLess:ordering -> bool) LT=        T)
+ ((orderingIsLess:ordering -> bool) LESS=        T)
 /\ ((orderingIsLess:ordering -> bool) _=        F)`;
 
 val _ = Define `
- ((orderingIsGreater:ordering -> bool) GT=     T)
+ ((orderingIsGreater:ordering -> bool) GREATER=     T)
 /\ ((orderingIsGreater:ordering -> bool) _=     F)`;
 
 val _ = Define `
- ((orderingIsEqual:ordering -> bool) EQ=       T)
+ ((orderingIsEqual:ordering -> bool) EQUAL=       T)
 /\ ((orderingIsEqual:ordering -> bool) _=       F)`;
 
 
 val _ = Define `
- ((ordering_cases:ordering -> 'a -> 'a -> 'a -> 'a) r lt eq gt=  
- (if orderingIsLess r then lt else
+ ((ordering_cases:ordering -> 'a -> 'a -> 'a -> 'a) r lt eq gt=
+   (if orderingIsLess r then lt else
   if orderingIsEqual r then eq else gt))`;
 
 
@@ -116,13 +115,13 @@ val _ = Hol_datatype `
 
 
 val _ = Define `
- ((genericCompare:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a -> 'a -> ordering) (less: 'a -> 'a -> bool) (equal: 'a -> 'a -> bool) (x : 'a) (y : 'a)=  
- (if less x y then
-    LT
+ ((genericCompare:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a -> 'a -> ordering) (less: 'a -> 'a -> bool) (equal: 'a -> 'a -> bool) (x : 'a) (y : 'a)=
+   (if less x y then
+    LESS
   else if equal x y then
-    EQ
+    EQUAL
   else
-    GT))`;
+    GREATER))`;
 
 
 
@@ -141,9 +140,9 @@ lemma ord_OK_2: (
 (* let's derive a compare function from the Ord type-class *)
 (*val ordCompare : forall 'a. Eq 'a, Ord 'a => 'a -> 'a -> ordering*)
 val _ = Define `
- ((ordCompare:'a Ord_class -> 'a -> 'a -> ordering)dict_Basic_classes_Ord_a x y=  
- (if ( dict_Basic_classes_Ord_a.isLess_method x y) then LT else
-  if (x = y) then EQ else GT))`;
+ ((ordCompare:'a Ord_class -> 'a -> 'a -> ordering)dict_Basic_classes_Ord_a x y=
+   (if ( dict_Basic_classes_Ord_a.isLess_method x y) then LESS else
+  if (x = y) then EQUAL else GREATER))`;
 
 
 val _ = Hol_datatype `
@@ -194,10 +193,10 @@ val _ = Define `
 end*)
 
 val _ = Define `
- ((boolCompare:bool -> bool -> ordering) T T=  EQ)
-/\ ((boolCompare:bool -> bool -> ordering) T F=  GT)
-/\ ((boolCompare:bool -> bool -> ordering) F T=  LT)
-/\ ((boolCompare:bool -> bool -> ordering) F F=  EQ)`;
+ ((boolCompare:bool -> bool -> ordering) T T=  EQUAL)
+/\ ((boolCompare:bool -> bool -> ordering) T F=  GREATER)
+/\ ((boolCompare:bool -> bool -> ordering) F T=  LESS)
+/\ ((boolCompare:bool -> bool -> ordering) F F=  EQUAL)`;
 
 
 (* strings *)
@@ -215,11 +214,11 @@ val _ = Define `
 
 (*val pairCompare : forall 'a 'b. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('a * 'b) -> ('a * 'b) -> ordering*)
 val _ = Define `
- ((pairCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) -> 'a#'b -> 'a#'b -> ordering) cmpa cmpb (a1, b1) (a2, b2)=  
- ((case cmpa a1 a2 of
-      LT => LT
-    | GT => GT
-    | EQ => cmpb b1 b2
+ ((pairCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) -> 'a#'b -> 'a#'b -> ordering) cmpa cmpb (a1, b1) (a2, b2)=
+   ((case cmpa a1 a2 of
+      LESS => LESS
+    | GREATER => GREATER
+    | EQUAL => cmpb b1 b2
   )))`;
 
 
@@ -268,8 +267,8 @@ val _ = Define `
 
 (*val tripleCompare : forall 'a 'b 'c. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> ordering*)
 val _ = Define `
- ((tripleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) -> 'a#'b#'c -> 'a#'b#'c -> ordering) cmpa cmpb cmpc (a1, b1, c1) (a2, b2, c2)=  
- (pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2))))`;
+ ((tripleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) -> 'a#'b#'c -> 'a#'b#'c -> ordering) cmpa cmpb cmpc (a1, b1, c1) (a2, b2, c2)=
+   (pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2))))`;
 
 
 val _ = Define `
@@ -323,8 +322,8 @@ val _ = Define `
 (*val quadrupleCompare : forall 'a 'b 'c 'd. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) ->
                                               ('d -> 'd -> ordering) -> ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> ordering*)
 val _ = Define `
- ((quadrupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> ordering) cmpa cmpb cmpc cmpd (a1, b1, c1, d1) (a2, b2, c2, d2)=  
- (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc cmpd)) (a1, (b1, (c1, d1))) (a2, (b2, (c2, d2)))))`;
+ ((quadrupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> ordering) cmpa cmpb cmpc cmpd (a1, b1, c1, d1) (a2, b2, c2, d2)=
+   (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc cmpd)) (a1, (b1, (c1, d1))) (a2, (b2, (c2, d2)))))`;
 
 
 val _ = Define `
@@ -380,8 +379,8 @@ val _ = Define `
 (*val quintupleCompare : forall 'a 'b 'c 'd 'e. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) ->
                                               ('d -> 'd -> ordering) -> ('e -> 'e -> ordering) -> ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> ordering*)
 val _ = Define `
- ((quintupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> ordering) cmpa cmpb cmpc cmpd cmpe (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)=  
- (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd cmpe))) (a1, (b1, (c1, (d1, e1)))) (a2, (b2, (c2, (d2, e2))))))`;
+ ((quintupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> ordering) cmpa cmpb cmpc cmpd cmpe (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)=
+   (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd cmpe))) (a1, (b1, (c1, (d1, e1)))) (a2, (b2, (c2, (d2, e2))))))`;
 
 
 val _ = Define `
@@ -444,8 +443,8 @@ val _ = Define `
                                               ('d -> 'd -> ordering) -> ('e -> 'e -> ordering) -> ('f -> 'f -> ordering) ->
                                               ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> ordering*)
 val _ = Define `
- ((sextupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) ->('f -> 'f -> ordering) -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> ordering) cmpa cmpb cmpc cmpd cmpe cmpf (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)=  
- (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd (pairCompare cmpe cmpf)))) (a1, (b1, (c1, (d1, (e1, f1))))) (a2, (b2, (c2, (d2, (e2, f2)))))))`;
+ ((sextupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) ->('f -> 'f -> ordering) -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> ordering) cmpa cmpb cmpc cmpd cmpe cmpf (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)=
+   (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd (pairCompare cmpe cmpf)))) (a1, (b1, (c1, (d1, (e1, f1))))) (a2, (b2, (c2, (d2, (e2, f2)))))))`;
 
 
 val _ = Define `
diff --git a/snapshots/hol4/lem/hol-lib/lem_eitherScript.sml b/snapshots/hol4/lem/hol-lib/lem_eitherScript.sml
index 15437410..cad53888 100644
--- a/snapshots/hol4/lem/hol-lib/lem_eitherScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_eitherScript.sml
@@ -27,8 +27,8 @@ val _ = new_theory "lem_either"
 (*val eitherEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> (either 'a 'b) -> (either 'a 'b) -> bool*)
 
 val _ = Define `
- ((eitherEqualBy:('a -> 'a -> bool) ->('b -> 'b -> bool) ->('a,'b)sum ->('a,'b)sum -> bool) eql eqr (left: ('a, 'b) sum) (right: ('a, 'b) sum)=  
- ((case (left, right) of
+ ((eitherEqualBy:('a -> 'a -> bool) ->('b -> 'b -> bool) ->('a,'b)sum ->('a,'b)sum -> bool) eql eqr (left: ('a, 'b) sum) (right: ('a, 'b) sum)=
+   ((case (left, right) of
       (INL l, INL l') => eql l l'
     | (INR r, INR r') => eqr r r'
     | _ => F
@@ -37,10 +37,10 @@ val _ = Define `
 (*let eitherEqual=  eitherEqualBy (=) (=)*)
 
 val _ = Define `
- ((either_setElemCompare:('d -> 'b -> lem_basic_classes$ordering) ->('c -> 'a -> lem_basic_classes$ordering) ->('d,'c)sum ->('b,'a)sum -> lem_basic_classes$ordering) cmpa cmpb (INL x') (INL y')=  (cmpa x' y'))
-/\ ((either_setElemCompare:('d -> 'b -> lem_basic_classes$ordering) ->('c -> 'a -> lem_basic_classes$ordering) ->('d,'c)sum ->('b,'a)sum -> lem_basic_classes$ordering) cmpa cmpb (INR x') (INR y')=  (cmpb x' y'))
-/\ ((either_setElemCompare:('d -> 'b -> lem_basic_classes$ordering) ->('c -> 'a -> lem_basic_classes$ordering) ->('d,'c)sum ->('b,'a)sum -> lem_basic_classes$ordering) cmpa cmpb (INL _) (INR _)=  LT)
-/\ ((either_setElemCompare:('d -> 'b -> lem_basic_classes$ordering) ->('c -> 'a -> lem_basic_classes$ordering) ->('d,'c)sum ->('b,'a)sum -> lem_basic_classes$ordering) cmpa cmpb (INR _) (INL _)=  GT)`;
+ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INL x') (INL y')=  (cmpa x' y'))
+/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INR x') (INR y')=  (cmpb x' y'))
+/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INL _) (INR _)=  LESS)
+/\ ((either_setElemCompare:('d -> 'b -> ordering) ->('c -> 'a -> ordering) ->('d,'c)sum ->('b,'a)sum -> ordering) cmpa cmpb (INR _) (INL _)=  GREATER)`;
 
                            
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml
index 6543ef87..c77c977c 100644
--- a/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_function_extraScript.sml
@@ -19,7 +19,7 @@ val _ = new_theory "lem_function_extra"
 (* getting a unique value  *)
 (* ----------------------- *)
 
-(*val THE : forall 'a. ('a -> bool) -> Maybe.maybe 'a*)
+(*val THE : forall 'a. ('a -> bool) -> maybe 'a*)
 
 val _ = export_theory()
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_listScript.sml b/snapshots/hol4/lem/hol-lib/lem_listScript.sml
index f2ba75d6..1b8f25f3 100644
--- a/snapshots/hol4/lem/hol-lib/lem_listScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_listScript.sml
@@ -43,8 +43,8 @@ val _ = new_theory "lem_list"
 (* ----------------------- *)
 
 (*val length : forall 'a. list 'a -> nat*)
-(*let rec length l= 
-  match l with
+(*let rec length l=
+   match l with
     | [] -> 0
     | x :: xs -> (Instance_Num_NumAdd_nat.+) (length xs) 1
   end*)
@@ -68,18 +68,18 @@ val _ = new_theory "lem_list"
 (* compare                 *)
 (* ----------------------- *)
 
-(*val lexicographicCompare : forall 'a. Ord 'a => list 'a -> list 'a -> Basic_classes.ordering*)
-(*val lexicographicCompareBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> list 'a -> list 'a -> Basic_classes.ordering*)
+(*val lexicographicCompare : forall 'a. Ord 'a => list 'a -> list 'a -> ordering*)
+(*val lexicographicCompareBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a -> ordering*)
 
  val _ = Define `
- ((lexicographic_compare:('a -> 'a -> lem_basic_classes$ordering) -> 'a list -> 'a list -> lem_basic_classes$ordering) cmp ([]) ([])=  EQ)
-/\ ((lexicographic_compare:('a -> 'a -> lem_basic_classes$ordering) -> 'a list -> 'a list -> lem_basic_classes$ordering) cmp ([]) (_::_)=  LT)
-/\ ((lexicographic_compare:('a -> 'a -> lem_basic_classes$ordering) -> 'a list -> 'a list -> lem_basic_classes$ordering) cmp (_::_) ([])=  GT)
-/\ ((lexicographic_compare:('a -> 'a -> lem_basic_classes$ordering) -> 'a list -> 'a list -> lem_basic_classes$ordering) cmp (x::xs) (y::ys)=  ((
+ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp ([]) ([])=  EQUAL)
+/\ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp ([]) (_::_)=  LESS)
+/\ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp (_::_) ([])=  GREATER)
+/\ ((lexicographic_compare:('a -> 'a -> ordering) -> 'a list -> 'a list -> ordering) cmp (x::xs) (y::ys)=  ((
       (case cmp x y of 
-          LT => LT
-        | GT => GT
-        | EQ => lexicographic_compare cmp xs ys
+          LESS => LESS
+        | GREATER => GREATER
+        | EQUAL => lexicographic_compare cmp xs ys
       )
     )))`;
 
@@ -104,7 +104,7 @@ val _ = new_theory "lem_list"
 
 
 val _ = Define `
-((instance_Basic_classes_Ord_list_dict:'a lem_basic_classes$Ord_class ->('a list)lem_basic_classes$Ord_class)dict_Basic_classes_Ord_a= (<|
+((instance_Basic_classes_Ord_list_dict:'a Ord_class ->('a list)Ord_class)dict_Basic_classes_Ord_a= (<|
 
   compare_method := (lexicographic_compare  
   dict_Basic_classes_Ord_a.compare_method);
@@ -256,7 +256,7 @@ end*)
 
 (* get the initial part and the last element of the list in a safe way *)
 
-(*val dest_init : forall 'a. list 'a -> Maybe.maybe (list 'a * 'a)*) 
+(*val dest_init : forall 'a. list 'a -> maybe (list 'a * 'a)*) 
 
  val _ = Define `
  ((dest_init_aux:'a list -> 'a -> 'a list -> 'a list#'a) rev_init last_elem_seen ([])=  (REVERSE rev_init, last_elem_seen))
@@ -277,7 +277,7 @@ val _ = Define `
 (* index / nth with maybe   *)
 (* ------------------------- *)
 
-(*val index : forall 'a. list 'a -> nat -> Maybe.maybe 'a*)
+(*val index : forall 'a. list 'a -> nat -> maybe 'a*)
 
  val _ = Define `
  ((list_index:'a list -> num -> 'a option) ([]) n=  NONE)
@@ -307,7 +307,7 @@ val _ = Define `
 (* ------------------------- *)
 
 (* findIndex returns the first index of a list that satisfies a given predicate. *)
-(*val findIndex : forall 'a. ('a -> bool) -> list 'a -> Maybe.maybe nat*)
+(*val findIndex : forall 'a. ('a -> bool) -> list 'a -> maybe nat*)
 val _ = Define `
  ((find_index:('a -> bool) -> 'a list ->(num)option) P l=  ((case find_indices P l of
     [] => NONE
@@ -325,7 +325,7 @@ val _ = Define `
 (* elemIndex                 *)
 (* ------------------------- *)
 
-(*val elemIndex : forall 'a. Eq 'a => 'a -> list 'a -> Maybe.maybe nat*)
+(*val elemIndex : forall 'a. Eq 'a => 'a -> list 'a -> maybe nat*)
 
 
 (* ========================================================================== *)
@@ -340,8 +340,8 @@ val _ = Define `
 (*val genlist : forall 'a. (nat -> 'a) -> nat -> list 'a*)
 
 
-(*let rec genlist f n= 
-  match n with
+(*let rec genlist f n=
+   match n with
     | 0 -> []
     | n' + 1 -> snoc (f n') (genlist f n')
   end*)
@@ -352,8 +352,8 @@ val _ = Define `
 (* ------------------------- *)
 
 (*val replicate : forall 'a. nat -> 'a -> list 'a*)
-(*let rec replicate n x= 
-  match n with
+(*let rec replicate n x=
+   match n with
     | 0 -> []
     | n' + 1 -> x :: replicate n' x
   end*)
@@ -372,8 +372,8 @@ val _ = Define `
    in [xs], the original list and the empty one are returned. *)
 (*val splitAtAcc : forall 'a. list 'a -> nat -> list 'a -> (list 'a * list 'a)*)
  val splitAtAcc_defn = Hol_defn "splitAtAcc" `
- ((splitAtAcc:'a list -> num -> 'a list -> 'a list#'a list) revAcc n l=  
-  ((case l of
+ ((splitAtAcc:'a list -> num -> 'a list -> 'a list#'a list) revAcc n l= 
+   ((case l of
       []    => (REVERSE revAcc, [])
     | x::xs => if n <=( 0 : num) then (REVERSE revAcc, l) else splitAtAcc (x::revAcc) (n -( 1 : num)) xs
   )))`;
@@ -381,8 +381,8 @@ val _ = Define `
 val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn splitAtAcc_defn;
 
 (*val splitAt : forall 'a. nat -> list 'a -> (list 'a * list 'a)*)
-(*let rec splitAt n l=  
-   splitAtAcc [] n l*)
+(*let rec splitAt n l= 
+    splitAtAcc [] n l*)
 
 
 (* ------------------------- *)
@@ -407,10 +407,10 @@ val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn
 
 (*val splitWhile_tr : forall 'a. ('a -> bool) -> list 'a -> list 'a -> (list 'a * list 'a)*)
  val _ = Define `
- ((splitWhile_tr:('a -> bool) -> 'a list -> 'a list -> 'a list#'a list) p ([]) acc= 
-    (REVERSE acc, []))
-/\ ((splitWhile_tr:('a -> bool) -> 'a list -> 'a list -> 'a list#'a list) p (x::xs) acc=    
- (if p x then
+ ((splitWhile_tr:('a -> bool) -> 'a list -> 'a list -> 'a list#'a list) p ([]) acc=
+     (REVERSE acc, []))
+/\ ((splitWhile_tr:('a -> bool) -> 'a list -> 'a list -> 'a list#'a list) p (x::xs) acc=
+     (if p x then
       splitWhile_tr p xs (x::acc)
     else
       (REVERSE acc, (x::xs))))`;
@@ -448,8 +448,8 @@ end*)
 (* update                    *)
 (* ------------------------- *)
 (*val update : forall 'a. list 'a -> nat -> 'a -> list 'a*)
-(*let rec update l n e=  
-  match l with
+(*let rec update l n e= 
+   match l with
     | []      -> []
     | x :: xs -> if (Instance_Basic_classes_Eq_nat.=) n 0 then e :: xs else x :: (update xs ((Instance_Num_NumMinus_nat.-) n 1) e)
 end*)
@@ -492,7 +492,7 @@ val _ = Define `
 (* ------------------------- *)
 (* Find                      *)
 (* ------------------------- *)
-(*val find : forall 'a. ('a -> bool) -> list 'a -> Maybe.maybe 'a*) (* previously not of maybe type *)
+(*val find : forall 'a. ('a -> bool) -> list 'a -> maybe 'a*) (* previously not of maybe type *)
  val _ = Define `
  ((list_find_opt:('a -> bool) -> 'a list -> 'a option) P ([])=  NONE)
 /\ ((list_find_opt:('a -> bool) -> 'a list -> 'a option) P (x :: xs)=  (if P x then SOME x else list_find_opt P xs))`;
@@ -502,8 +502,8 @@ val _ = Define `
 (* ----------------------------- *)
 (* Lookup in an associative list *)
 (* ----------------------------- *)
-(*val lookup   : forall 'a 'b. Eq 'a              => 'a -> list ('a * 'b) -> Maybe.maybe 'b*)
-(*val lookupBy : forall 'a 'b. ('a -> 'a -> bool) -> 'a -> list ('a * 'b) -> Maybe.maybe 'b*)
+(*val lookup   : forall 'a 'b. Eq 'a              => 'a -> list ('a * 'b) -> maybe 'b*)
+(*val lookupBy : forall 'a 'b. ('a -> 'a -> bool) -> 'a -> list ('a * 'b) -> maybe 'b*)
 
 (* DPM: eta-expansion for Coq backend type-inference. *)
 val _ = Define `
@@ -536,7 +536,7 @@ val _ = Define `
 (* with certain property     *)
 (* ------------------------- *)
 
-(*val deleteFirst : forall 'a. ('a -> bool) -> list 'a -> Maybe.maybe (list 'a)*) 
+(*val deleteFirst : forall 'a. ('a -> bool) -> list 'a -> maybe (list 'a)*) 
  val _ = Define `
  ((list_delete_first:('a -> bool) -> 'a list ->('a list)option) P ([])=  NONE)
 /\ ((list_delete_first:('a -> bool) -> 'a list ->('a list)option) P (x :: xs)=  (if (P x) then SOME xs else OPTION_MAP (\ xs' .  x :: xs') (list_delete_first P xs)))`;
@@ -583,18 +583,18 @@ end*)
 (* ------------------------- *)
 
 (*val allDistinct : forall 'a. Eq 'a => list 'a -> bool*)
-(*let rec allDistinct l=  
-  match l with
+(*let rec allDistinct l= 
+   match l with
     | [] -> true
     | (x::l') -> not (elem x l') && allDistinct l'
   end*)
 
 (* some more useful functions *)
-(*val mapMaybe : forall 'a 'b. ('a -> Maybe.maybe 'b) -> list 'a -> list 'b*)
+(*val mapMaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> list 'b*)
  val mapMaybe_defn = Defn.Hol_multi_defns `
  ((mapMaybe:('a -> 'b option) -> 'a list -> 'b list) f ([])=  ([]))
-/\ ((mapMaybe:('a -> 'b option) -> 'a list -> 'b list) f (x::xs)=      
- ((case f x of
+/\ ((mapMaybe:('a -> 'b option) -> 'a list -> 'b list) f (x::xs)=
+       ((case f x of
         NONE => mapMaybe f xs
       | SOME y => y :: (mapMaybe f xs)
       )))`;
@@ -613,8 +613,8 @@ val _ = Define `
 
 (*val deletes: forall 'a. Eq 'a => list 'a -> list 'a -> list 'a*)
 val _ = Define `
- ((deletes:'a list -> 'a list -> 'a list) xs ys=  
- (FOLDL (combin$C (list_delete (=))) xs ys))`;
+ ((deletes:'a list -> 'a list -> 'a list) xs ys=
+   (FOLDL (combin$C (list_delete (=))) xs ys))`;
 
 
 (* ========================================================================== *)
@@ -762,14 +762,14 @@ val intersect : forall 'a. list 'a -> list 'a -> list 'a
 
 *)
 
-(*val     catMaybes : forall 'a. list (Maybe.maybe 'a) -> list 'a*)
+(*val     catMaybes : forall 'a. list (maybe 'a) -> list 'a*)
  val catMaybes_defn = Defn.Hol_multi_defns `
- ((catMaybes:('a option)list -> 'a list) ([])=        
- ([]))
-/\ ((catMaybes:('a option)list -> 'a list) (NONE :: xs')=        
- (catMaybes xs'))
-/\ ((catMaybes:('a option)list -> 'a list) (SOME x :: xs')=        
- (x :: catMaybes xs'))`;
+ ((catMaybes:('a option)list -> 'a list) ([])=
+         ([]))
+/\ ((catMaybes:('a option)list -> 'a list) (NONE :: xs')=
+         (catMaybes xs'))
+/\ ((catMaybes:('a option)list -> 'a list) (SOME x :: xs')=
+         (x :: catMaybes xs'))`;
 
 val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) catMaybes_defn;
 val _ = export_theory()
diff --git a/snapshots/hol4/lem/hol-lib/lem_list_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_list_extraScript.sml
index b8e452d3..123d8a78 100644
--- a/snapshots/hol4/lem/hol-lib/lem_list_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_list_extraScript.sml
@@ -94,10 +94,10 @@ val _ = Define `
 
 end*)
 
-(*val     unfoldr: forall 'a 'b. ('a -> Maybe.maybe ('b * 'a)) -> 'a -> list 'b*)
+(*val     unfoldr: forall 'a 'b. ('a -> maybe ('b * 'a)) -> 'a -> list 'b*)
  val unfoldr_defn = Hol_defn "unfoldr" `
- ((unfoldr:('a ->('b#'a)option) -> 'a -> 'b list) f x=  
- ((case f x of
+ ((unfoldr:('a ->('b#'a)option) -> 'a -> 'b list) f x=
+   ((case f x of
       SOME (y, x') =>
         y :: unfoldr f x'
     | NONE =>
diff --git a/snapshots/hol4/lem/hol-lib/lem_machine_wordScript.sml b/snapshots/hol4/lem/hol-lib/lem_machine_wordScript.sml
index c169e9a8..294bf8ca 100644
--- a/snapshots/hol4/lem/hol-lib/lem_machine_wordScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_machine_wordScript.sml
@@ -23,7 +23,7 @@ end*)
 
 (*val native_size : forall 'a. nat*)
 
-(*val ocaml_inject : forall 'a. nat * Num.natural -> mword 'a*)
+(*val ocaml_inject : forall 'a. nat * natural -> mword 'a*)
 
 (* A singleton type family that can be used to carry a size as the type parameter *)
 
@@ -313,25 +313,25 @@ val _ = Define `
 (* Conversions                                                    *)
 (******************************************************************)
 
-(*val signedIntegerFromWord : forall 'a. mword 'a -> Num.integer*)
+(*val signedIntegerFromWord : forall 'a. mword 'a -> integer*)
 
-(*val unsignedIntegerFromWord : forall 'a. mword 'a -> Num.integer*)
+(*val unsignedIntegerFromWord : forall 'a. mword 'a -> integer*)
 
 (* Version without typeclass constraint so that we can derive operations
    in Lem for one of the theorem provers without requiring it. *)
-(*val proverWordFromInteger : forall 'a. Num.integer -> mword 'a*)
+(*val proverWordFromInteger : forall 'a. integer -> mword 'a*)
 
-(*val wordFromInteger : forall 'a. Size 'a => Num.integer -> mword 'a*)
+(*val wordFromInteger : forall 'a. Size 'a => integer -> mword 'a*)
 (* The OCaml version is defined after the arithmetic operations, below. *)
 
-(*val naturalFromWord : forall 'a. mword 'a -> Num.natural*)
+(*val naturalFromWord : forall 'a. mword 'a -> natural*)
 
-(*val wordFromNatural : forall 'a. Size 'a => Num.natural -> mword 'a*)
+(*val wordFromNatural : forall 'a. Size 'a => natural -> mword 'a*)
 
 (*val wordToHex : forall 'a. mword 'a -> string*)
 
 val _ = Define `
-((instance_Show_Show_Machine_word_mword_dict:('a words$word)lem_show$Show_class)= (<|
+((instance_Show_Show_Machine_word_mword_dict:('a words$word)Show_class)= (<|
 
   show_method := words$word_to_hex_string|>))`;
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_mapScript.sml b/snapshots/hol4/lem/hol-lib/lem_mapScript.sml
index a85a9d67..e05af7f2 100644
--- a/snapshots/hol4/lem/hol-lib/lem_mapScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_mapScript.sml
@@ -30,7 +30,7 @@ val _ = new_theory "lem_map"
 (* -------------------------------------------------------------------------- *)
 
 (*class ( MapKeyType 'a )
-  val {ocaml;coq} mapKeyCompare : 'a -> 'a -> Basic_classes.ordering
+  val {ocaml;coq} mapKeyCompare : 'a -> 'a -> ordering
 end*)
 
 (* -------------------------------------------------------------------------- *)
@@ -38,7 +38,7 @@ end*)
 (* -------------------------------------------------------------------------- *)
 
 (*val empty : forall 'k 'v. MapKeyType 'k => map 'k 'v*)
-(*val emptyBy : forall 'k 'v. ('k -> 'k -> Basic_classes.ordering) -> map 'k 'v*)
+(*val emptyBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v*)
 
 
 (* -------------------------------------------------------------------------- *)
@@ -67,9 +67,9 @@ end*)
 (* lookup                                                                     *)
 (* -------------------------------------------------------------------------- *)
 
-(*val lookupBy : forall 'k 'v. ('k -> 'k -> Basic_classes.ordering) -> 'k -> map 'k 'v -> Maybe.maybe 'v*)
+(*val lookupBy : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> maybe 'v*)
 
-(*val lookup          : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> Maybe.maybe 'v*)
+(*val lookup          : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> maybe 'v*)
 
 (* -------------------------------------------------------------------------- *)
 (* findWithDefault                                                            *)
@@ -90,15 +90,15 @@ end*)
 (* -------------------------------------------------------------------------- *)
 
 (*val toSet : forall 'k 'v. MapKeyType 'k, SetType 'k, SetType 'v => map 'k 'v -> set ('k * 'v)*) 
-(*val toSetBy : forall 'k 'v. (('k * 'v) -> ('k * 'v) -> Basic_classes.ordering) -> map 'k 'v -> set ('k * 'v)*)
+(*val toSetBy : forall 'k 'v. (('k * 'v) -> ('k * 'v) -> ordering) -> map 'k 'v -> set ('k * 'v)*)
 
 
-(*val domainBy : forall 'k 'v. ('k -> 'k -> Basic_classes.ordering) -> map 'k 'v -> set 'k*)
+(*val domainBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v -> set 'k*)
 (*val domain : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> set 'k*)
 
 
 (*val range : forall 'k 'v. MapKeyType 'k, SetType 'v => map 'k 'v -> set 'v*)
-(*val rangeBy : forall 'k 'v. ('v -> 'v -> Basic_classes.ordering) -> map 'k 'v -> set 'v*)
+(*val rangeBy : forall 'k 'v. ('v -> 'v -> ordering) -> map 'k 'v -> set 'v*)
 
 
 (* -------------------------------------------------------------------------- *)
@@ -122,7 +122,7 @@ end*)
 (* -------------------------------------------------------------------------- *)
 (* Set-like operations.                                                       *)
 (* -------------------------------------------------------------------------- *)
-(*val deleteBy         : forall 'k 'v. ('k -> 'k -> Basic_classes.ordering) -> 'k -> map 'k 'v -> map 'k 'v*)
+(*val deleteBy         : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> map 'k 'v*)
 (*val delete           : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> map 'k 'v*)
 (*val deleteSwap      : forall 'k 'v. MapKeyType 'k => map 'k 'v -> 'k -> map 'k 'v*)
 
@@ -146,8 +146,8 @@ end*)
 
 (* instance of SetType *)
 val _ = Define `
- ((map_setElemCompare:(('d#'c)set ->('b#'a)set -> 'e) ->('d,'c)fmap ->('b,'a)fmap -> 'e) cmp x y=  
- (cmp (FMAP_TO_SET x) (FMAP_TO_SET y)))`;
+ ((map_setElemCompare:(('d#'c)set ->('b#'a)set -> 'e) ->('d,'c)fmap ->('b,'a)fmap -> 'e) cmp x y=
+   (cmp (FMAP_TO_SET x) (FMAP_TO_SET y)))`;
 
 val _ = export_theory()
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml
index 57a258f8..7e32efb7 100644
--- a/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml
@@ -16,7 +16,7 @@ val _ = new_theory "lem_map_extra"
 (* find                                                                       *)
 (* -------------------------------------------------------------------------- *)
 
-(*val find : forall 'k 'v. MapKeyType 'k => 'k -> Map.map 'k 'v -> 'v*)
+(*val find : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> 'v*)
 (*let find k m=  match (lookup k m) with Just x -> x | Nothing -> failwith "Map_extra.find" end*)
 
 
@@ -26,7 +26,7 @@ val _ = new_theory "lem_map_extra"
 (* -------------------------------------------------------------------------- *)
 
 
-(*val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> Map.map 'k 'v*)
+(*val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> map 'k 'v*)
 (*let fromSet f s=  Set_helpers.fold (fun k m -> Map.insert k (f k) m) s Map.empty*)
 
 (*
@@ -38,7 +38,7 @@ assert fromSet_1: (fromSet succ {(2:nat); 3; 4}) = Map.fromList [(2,3); (3, 4);
 (* fold                                                                       *)
 (* -------------------------------------------------------------------------- *)
 
-(*val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> Map.map 'k 'v -> 'r -> 'r*)
+(*val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> map 'k 'v -> 'r -> 'r*)
 val _ = Define `
  ((fold:('k -> 'v -> 'r -> 'r) ->('k,'v)fmap -> 'r -> 'r) f m v=  (ITSET (\ (k, v) r .  f k v r) (FMAP_TO_SET m) v))`;
 
@@ -48,17 +48,17 @@ assert fold_1: (fold (fun k v a -> (a+k)) (Map.fromList [((2:nat),(3:nat)); (3,
 assert fold_2: (fold (fun k v a -> (a+v)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 12)
 *)
 
-(*val toList: forall 'k 'v. MapKeyType 'k => Map.map 'k 'v -> list ('k * 'v)*)
+(*val toList: forall 'k 'v. MapKeyType 'k => map 'k 'v -> list ('k * 'v)*)
 (* declare compile_message toList = "Map_extra.toList is only defined for the ocaml, isabelle and coq backend" *)
 
 (* more 'map' functions *)
 
 (* TODO: this function is in map_extra rather than map just for implementation reasons *)
-(*val mapMaybe : forall 'a 'b 'c. MapKeyType 'a => ('a -> 'b -> Maybe.maybe 'c) -> Map.map 'a 'b -> Map.map 'a 'c*)
+(*val mapMaybe : forall 'a 'b 'c. MapKeyType 'a => ('a -> 'b -> maybe 'c) -> map 'a 'b -> map 'a 'c*)
 (* OLD: TODO: mapMaybe depends on toList that is not defined for hol and isabelle *)
 val _ = Define `
- ((option_map:('a -> 'b -> 'c option) ->('a,'b)fmap ->('a,'c)fmap) f m=  
- (FOLDL
+ ((option_map:('a -> 'b -> 'c option) ->('a,'b)fmap ->('a,'c)fmap) f m=
+   (FOLDL
     (\ m' (k, v) . 
       (case f k v of
           NONE => m'
diff --git a/snapshots/hol4/lem/hol-lib/lem_maybeScript.sml b/snapshots/hol4/lem/hol-lib/lem_maybeScript.sml
index 29562d66..bcf4348b 100644
--- a/snapshots/hol4/lem/hol-lib/lem_maybeScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_maybeScript.sml
@@ -33,29 +33,29 @@ val _ = Define `
 
 
 val _ = Define `
- ((maybeCompare:('b -> 'a -> lem_basic_classes$ordering) -> 'b option -> 'a option -> lem_basic_classes$ordering) cmp NONE NONE=  EQ)
-/\ ((maybeCompare:('b -> 'a -> lem_basic_classes$ordering) -> 'b option -> 'a option -> lem_basic_classes$ordering) cmp NONE (SOME _)=  LT)
-/\ ((maybeCompare:('b -> 'a -> lem_basic_classes$ordering) -> 'b option -> 'a option -> lem_basic_classes$ordering) cmp (SOME _) NONE=  GT)
-/\ ((maybeCompare:('b -> 'a -> lem_basic_classes$ordering) -> 'b option -> 'a option -> lem_basic_classes$ordering) cmp (SOME x') (SOME y')=  (cmp x' y'))`;
+ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp NONE NONE=  EQUAL)
+/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp NONE (SOME _)=  LESS)
+/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp (SOME _) NONE=  GREATER)
+/\ ((maybeCompare:('b -> 'a -> ordering) -> 'b option -> 'a option -> ordering) cmp (SOME x') (SOME y')=  (cmp x' y'))`;
 
 
 val _ = Define `
-((instance_Basic_classes_Ord_Maybe_maybe_dict:'a lem_basic_classes$Ord_class ->('a option)lem_basic_classes$Ord_class)dict_Basic_classes_Ord_a= (<|
+((instance_Basic_classes_Ord_Maybe_maybe_dict:'a Ord_class ->('a option)Ord_class)dict_Basic_classes_Ord_a= (<|
 
   compare_method := (maybeCompare  
   dict_Basic_classes_Ord_a.compare_method);
 
   isLess_method := (\ m1 .  (\ m2 .  maybeCompare  
-  dict_Basic_classes_Ord_a.compare_method m1 m2 = LT));
+  dict_Basic_classes_Ord_a.compare_method m1 m2 = LESS));
 
   isLessEqual_method := (\ m1 .  (\ m2 .  (let r = (maybeCompare  
-  dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = LT) \/ (r = EQ))));
+  dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = LESS) \/ (r = EQUAL))));
 
   isGreater_method := (\ m1 .  (\ m2 .  maybeCompare  
-  dict_Basic_classes_Ord_a.compare_method m1 m2 = GT));
+  dict_Basic_classes_Ord_a.compare_method m1 m2 = GREATER));
 
   isGreaterEqual_method := (\ m1 .  (\ m2 .  (let r = (maybeCompare  
-  dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = GT) \/ (r = EQ))))|>))`;
+  dict_Basic_classes_Ord_a.compare_method m1 m2) in (r = GREATER) \/ (r = EQUAL))))|>))`;
 
 
 (* ----------------------- *)
diff --git a/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml
index 6b04d291..22d7e061 100644
--- a/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml
@@ -16,7 +16,7 @@ val _ = new_theory "lem_maybe_extra"
 (* fromJust                *)
 (* ----------------------- *)
 
-(*val fromJust : forall 'a. Maybe.maybe 'a -> 'a*)
+(*val fromJust : forall 'a. maybe 'a -> 'a*)
 (*let fromJust op=  match op with | Just v -> v | Nothing -> failwith "fromJust of Nothing" end*)
 
 val _ = export_theory()
diff --git a/snapshots/hol4/lem/hol-lib/lem_numScript.sml b/snapshots/hol4/lem/hol-lib/lem_numScript.sml
index 9dcd0554..6064416b 100644
--- a/snapshots/hol4/lem/hol-lib/lem_numScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_numScript.sml
@@ -179,10 +179,10 @@ val _ = Hol_datatype `
 (*val natGreater : nat -> nat -> bool*)
 (*val natGreaterEqual : nat -> nat -> bool*)
 
-(*val natCompare : nat -> nat -> Basic_classes.ordering*)
+(*val natCompare : nat -> nat -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_nat_dict:(num)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_nat_dict:(num)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -259,8 +259,8 @@ val _ = Define `
 
 (*val gen_pow_aux : forall 'a. ('a -> 'a -> 'a) -> 'a -> 'a -> nat -> 'a*)
  val _ = Define `
- ((gen_pow_aux:('a -> 'a -> 'a) -> 'a -> 'a -> num -> 'a) (mul : 'a -> 'a -> 'a) (a : 'a) (b : 'a) (e : num)=   
- ((case e of
+ ((gen_pow_aux:('a -> 'a -> 'a) -> 'a -> 'a -> num -> 'a) (mul : 'a -> 'a -> 'a) (a : 'a) (b : 'a) (e : num)=
+    ((case e of
        0 => a (* cannot happen, call discipline guarentees e >= 1 *)
      | (SUC 0) => mul a b
      | (  (SUC(SUC e'))) => let e'' = (e DIV( 2 : num)) in
@@ -270,8 +270,8 @@ val _ = Define `
 
        
 val _ = Define `
- ((gen_pow:'a ->('a -> 'a -> 'a) -> 'a -> num -> 'a) (one1 : 'a) (mul : 'a -> 'a -> 'a) (b : 'a) (e : num) : 'a=  
-  (if e <( 0 : num) then one1 else 
+ ((gen_pow:'a ->('a -> 'a -> 'a) -> 'a -> num -> 'a) (one1 : 'a) (mul : 'a -> 'a -> 'a) (b : 'a) (e : num) : 'a= 
+   (if e <( 0 : num) then one1 else 
   if (e =( 0 : num)) then one1 else gen_pow_aux mul one1 b e))`;
 
 
@@ -288,7 +288,7 @@ val _ = Define `
 (*val natMax : nat -> nat -> nat*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_nat_dict:(num)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_nat_dict:(num)OrdMaxMin_class)= (<|
 
   max_method := MAX;
 
@@ -309,10 +309,10 @@ val _ = Define `
 (*val naturalGreater : natural -> natural -> bool*)
 (*val naturalGreaterEqual : natural -> natural -> bool*)
 
-(*val naturalCompare : natural -> natural -> Basic_classes.ordering*)
+(*val naturalCompare : natural -> natural -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_natural_dict:(num)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_natural_dict:(num)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -400,7 +400,7 @@ val _ = Define `
 (*val naturalMax : natural -> natural -> natural*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_natural_dict:(num)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_natural_dict:(num)OrdMaxMin_class)= (<|
 
   max_method := MAX;
 
@@ -421,10 +421,10 @@ val _ = Define `
 (*val intGreater : int -> int -> bool*)
 (*val intGreaterEqual : int -> int -> bool*)
 
-(*val intCompare : int -> int -> Basic_classes.ordering*)
+(*val intCompare : int -> int -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_int_dict:(int)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_int_dict:(int)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -527,7 +527,7 @@ val _ = Define `
 (*val intMax : int -> int -> int*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_int_dict:(int)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_int_dict:(int)OrdMaxMin_class)= (<|
 
   max_method := int_max;
 
@@ -546,10 +546,10 @@ val _ = Define `
 (*val int32Greater : int32 -> int32 -> bool*)
 (*val int32GreaterEqual : int32 -> int32 -> bool*)
 
-(*val int32Compare : int32 -> int32 -> Basic_classes.ordering*)
+(*val int32Compare : int32 -> int32 -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_int32_dict:(word32)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_int32_dict:(word32)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -660,7 +660,7 @@ val _ = Define `
 (*val int32Max : int32 -> int32 -> int32*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_int32_dict:(word32)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_int32_dict:(word32)OrdMaxMin_class)= (<|
 
   max_method := word_smax;
 
@@ -681,10 +681,10 @@ val _ = Define `
 (*val int64Greater : int64 -> int64 -> bool*)
 (*val int64GreaterEqual : int64 -> int64 -> bool*)
 
-(*val int64Compare : int64 -> int64 -> Basic_classes.ordering*)
+(*val int64Compare : int64 -> int64 -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_int64_dict:(word64)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_int64_dict:(word64)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -795,7 +795,7 @@ val _ = Define `
 (*val int64Max : int64 -> int64 -> int64*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_int64_dict:(word64)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_int64_dict:(word64)OrdMaxMin_class)= (<|
 
   max_method := word_smax;
 
@@ -818,10 +818,10 @@ val _ = Define `
 (*val integerGreater : integer -> integer -> bool*)
 (*val integerGreaterEqual : integer -> integer -> bool*)
 
-(*val integerCompare : integer -> integer -> Basic_classes.ordering*)
+(*val integerCompare : integer -> integer -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_integer_dict:(int)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_integer_dict:(int)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -924,7 +924,7 @@ val _ = Define `
 (*val integerMax : integer -> integer -> integer*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_integer_dict:(int)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_integer_dict:(int)OrdMaxMin_class)= (<|
 
   max_method := int_max;
 
@@ -948,10 +948,10 @@ val _ = Define `
 (*val rationalGreater : rational -> rational -> bool*)
 (*val rationalGreaterEqual : rational -> rational -> bool*)
 
-(*val rationalCompare : rational -> rational -> Basic_classes.ordering*)
+(*val rationalCompare : rational -> rational -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_rational_dict:(rat)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_rational_dict:(rat)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -1031,8 +1031,8 @@ val _ = Define `
 
 (*val rationalPowInteger : rational -> integer -> rational*)
  val rationalPowInteger_defn = Hol_defn "rationalPowInteger" `
- ((rationalPowInteger:rat -> int -> rat) b e=  
- (if e =( 0 : int) then( 1 : rat) else
+ ((rationalPowInteger:rat -> int -> rat) b e=
+   (if e =( 0 : int) then( 1 : rat) else
   if e >( 0 : int) then rationalPowInteger b (e -( 1 : int)) * b else
   rationalPowInteger b (e +( 1 : int)) / b))`;
 
@@ -1054,7 +1054,7 @@ val _ = Define `
 (*val rationalMax : rational -> rational -> rational*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_rational_dict:(rat)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_rational_dict:(rat)OrdMaxMin_class)= (<|
 
   max_method := (maxByLessEqual (<=));
 
@@ -1078,10 +1078,10 @@ val _ = Define `
 (*val realGreater : real -> real -> bool*)
 (*val realGreaterEqual : real -> real -> bool*)
 
-(*val realCompare : real -> real -> Basic_classes.ordering*)
+(*val realCompare : real -> real -> ordering*)
 
 val _ = Define `
-((instance_Basic_classes_Ord_Num_real_dict:(real)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Num_real_dict:(real)Ord_class)= (<|
 
   compare_method := (genericCompare (<) (=));
 
@@ -1163,8 +1163,8 @@ val _ = Define `
 
 (*val realPowInteger : real -> integer -> real*)
  val realPowInteger_defn = Hol_defn "realPowInteger" `
- ((realPowInteger:real -> int -> real) b e=  
- (if e =( 0 : int) then(real_of_num 1) else
+ ((realPowInteger:real -> int -> real) b e=
+   (if e =( 0 : int) then(real_of_num 1) else
   if e >( 0 : int) then realPowInteger b (e -( 1 : int)) * b else
   realPowInteger b (e +( 1 : int)) / b))`;
 
@@ -1186,7 +1186,7 @@ val _ = Define `
 (*val realMax : real -> real -> real*)
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Num_real_dict:(real)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Num_real_dict:(real)OrdMaxMin_class)= (<|
 
   max_method := max;
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml
index 69644f94..40356448 100644
--- a/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_num_extraScript.sml
@@ -17,18 +17,18 @@ val _ = new_theory "lem_num_extra"
 (*open import Num*)
 (*open import String*)
 
-(*val naturalOfString : string -> Num.natural*)
+(*val naturalOfString : string -> natural*)
 
-(*val integerOfString : string -> Num.integer*)
+(*val integerOfString : string -> integer*)
 
 
 (* Truncation integer division (round toward zero) *)
-(*val integerDiv_t: Num.integer -> Num.integer -> Num.integer*)
+(*val integerDiv_t: integer -> integer -> integer*)
 
 (* Truncation modulo *)
-(*val integerRem_t: Num.integer -> Num.integer -> Num.integer*)
+(*val integerRem_t: integer -> integer -> integer*)
 
 (* Flooring modulo *)
-(*val integerRem_f: Num.integer -> Num.integer -> Num.integer*)
+(*val integerRem_f: integer -> integer -> integer*)
 val _ = export_theory()
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_relationScript.sml b/snapshots/hol4/lem/hol-lib/lem_relationScript.sml
index e73b66ce..7d019b21 100644
--- a/snapshots/hol4/lem/hol-lib/lem_relationScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_relationScript.sml
@@ -393,7 +393,7 @@ val _ = Define `
 
 (*val transitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
 (*val transitiveClosureByEq  : forall 'a. ('a -> 'a -> bool) -> rel 'a 'a -> rel 'a 'a*)
-(*val transitiveClosureByCmp : forall 'a. ('a * 'a -> 'a * 'a -> Basic_classes.ordering) -> rel 'a 'a -> rel 'a 'a*)
+(*val transitiveClosureByCmp : forall 'a. ('a * 'a -> 'a * 'a -> ordering) -> rel 'a 'a -> rel 'a 'a*)
 
 
 (* ----------------------- *)
@@ -403,8 +403,8 @@ val _ = Define `
 (*val transitiveClosureAdd : forall 'a. SetType 'a, Eq 'a => 'a -> 'a -> rel 'a 'a -> rel 'a 'a*)
 
 val _ = Define `
- ((tc_insert:'a -> 'a ->('a#'a)set ->('a#'a)set) x y r=  
-  ((((((x,y) INSERT (r)))) UNION ((((({(x, z) | z | 
+ ((tc_insert:'a -> 'a ->('a#'a)set ->('a#'a)set) x y r= 
+   ((((((x,y) INSERT (r)))) UNION ((((({(x, z) | z | 
   (z IN range r) /\ ((y, z) IN r)})) UNION (({(z, y) | z | 
   (z IN domain r) /\ ((z, x) IN r)}))))))))`;
 
@@ -437,8 +437,8 @@ val _ = Define `
 
 (*val withoutTransitiveEdges: forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*)
 val _ = Define `
- ((withoutTransitiveEdges:('a#'a)set ->('a#'a)set) r=  
- (let tc1 = (tc r) in
+ ((withoutTransitiveEdges:('a#'a)set ->('a#'a)set) r=
+   (let tc1 = (tc r) in
   {(a, c) | a, c 
   | ((a, c) IN r) /\
    (! (b :: range r).
diff --git a/snapshots/hol4/lem/hol-lib/lem_setScript.sml b/snapshots/hol4/lem/hol-lib/lem_setScript.sml
index 7f553a68..c03aec5f 100644
--- a/snapshots/hol4/lem/hol-lib/lem_setScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_setScript.sml
@@ -49,7 +49,7 @@ val _ = new_theory "lem_set"
 (* Equality check          *)
 (* ----------------------- *)
 
-(*val setEqualBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> bool*)
+(*val setEqualBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
 
 (*val setEqual : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
 
@@ -58,7 +58,7 @@ val _ = new_theory "lem_set"
 (* ----------------------- *)
 
 (*val empty : forall 'a. SetType 'a => set 'a*) 
-(*val emptyBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a*)
+(*val emptyBy : forall 'a. ('a -> 'a -> ordering) -> set 'a*)
 
 (* ----------------------- *)
 (* any / all               *)
@@ -74,7 +74,7 @@ val _ = new_theory "lem_set"
 (* ----------------------- *)
 
 (*val IN [member] : forall 'a. SetType 'a => 'a -> set 'a -> bool*) 
-(*val memberBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> 'a -> set 'a -> bool*)
+(*val memberBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a -> bool*)
 
 (* ----------------------- *)
 (* not (IN)                *)
@@ -95,7 +95,7 @@ val _ = new_theory "lem_set"
 (* singleton                *)
 (* ------------------------ *)
 
-(*val singletonBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> 'a -> set 'a*)
+(*val singletonBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a*)
 (*val singleton : forall 'a. SetType 'a => 'a -> set 'a*)
 
 
@@ -117,7 +117,7 @@ val _ = new_theory "lem_set"
 (* union                    *)
 (* ------------------------ *)
 
-(*val unionBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> set 'a*)
+(*val unionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
 (*val union : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
 
 (* ----------------------- *)
@@ -150,13 +150,13 @@ val _ = Define `
 
 (*val split : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * set 'a*)
 val _ = Define `
- ((SET_SPLIT:'a lem_basic_classes$Ord_class -> 'a -> 'a set -> 'a set#'a set)dict_Basic_classes_Ord_a p s=  (SET_FILTER (
+ ((SET_SPLIT:'a Ord_class -> 'a -> 'a set -> 'a set#'a set)dict_Basic_classes_Ord_a p s=  (SET_FILTER (
   dict_Basic_classes_Ord_a.isGreater_method p) s, SET_FILTER (dict_Basic_classes_Ord_a.isLess_method p) s))`;
 
 
 (*val splitMember : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * bool * set 'a*)
 val _ = Define `
- ((splitMember:'a lem_basic_classes$Ord_class -> 'a -> 'a set -> 'a set#bool#'a set)dict_Basic_classes_Ord_a p s=  (SET_FILTER (
+ ((splitMember:'a Ord_class -> 'a -> 'a set -> 'a set#bool#'a set)dict_Basic_classes_Ord_a p s=  (SET_FILTER (
   dict_Basic_classes_Ord_a.isLess_method p) s, (p IN s), SET_FILTER (
   dict_Basic_classes_Ord_a.isGreater_method p) s))`;
 
@@ -165,8 +165,8 @@ val _ = Define `
 (* subset and proper subset *)
 (* ------------------------ *)
 
-(*val isSubsetOfBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> bool*)
-(*val isProperSubsetOfBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> bool*)
+(*val isSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
+(*val isProperSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*)
 
 (*val isSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
 (*val isProperSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*)
@@ -185,7 +185,7 @@ val _ = Define `
 (* ------------------------ *)
 
 (*val bigunion : forall 'a. SetType 'a => set (set 'a) -> set 'a*)
-(*val bigunionBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set (set 'a) -> set 'a*)
+(*val bigunionBy : forall 'a. ('a -> 'a -> ordering) -> set (set 'a) -> set 'a*)
 
 (*let bigunion bs=  {x | forall (s IN bs) (x IN s) | true}*)
 
@@ -206,7 +206,7 @@ val _ = Define `
 (* difference               *)
 (* ------------------------ *)
 
-(*val differenceBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> set 'a*)
+(*val differenceBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
 (*val difference : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
 
 (* ------------------------ *)
@@ -214,7 +214,7 @@ val _ = Define `
 (* ------------------------ *)
 
 (*val intersection : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*)
-(*val intersectionBy : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> set 'a*)
+(*val intersectionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*)
 
 
 (* ------------------------ *)
@@ -224,7 +224,7 @@ val _ = Define `
 (*val map : forall 'a 'b. SetType 'a, SetType 'b => ('a -> 'b) -> set 'a -> set 'b*) (* before image *)
 (*let map f s=  { f e | forall (e IN s) | true }*)
 
-(*val mapBy : forall 'a 'b. ('b -> 'b -> Basic_classes.ordering) -> ('a -> 'b) -> set 'a -> set 'b*) 
+(*val mapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> 'b) -> set 'a -> set 'b*) 
 
 
 (* ------------------------ *)
@@ -235,7 +235,7 @@ val _ = Define `
    it might be better to combine bigunion and map sometimes into a single operation. *)
 
 (*val bigunionMap : forall 'a 'b. SetType 'a, SetType 'b => ('a -> set 'b) -> set 'a -> set 'b*)
-(*val bigunionMapBy : forall 'a 'b. ('b -> 'b -> Basic_classes.ordering) -> ('a -> set 'b) -> set 'a -> set 'b*)
+(*val bigunionMapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> set 'b) -> set 'a -> set 'b*)
 
 (* ------------------------ *)
 (* mapMaybe and fromMaybe   *)
@@ -244,16 +244,16 @@ val _ = Define `
 (* If the mapping function returns Just x, x is added to the result
    set. If it returns Nothing, no element is added. *)
 
-(*val mapMaybe : forall 'a 'b. SetType 'a, SetType 'b => ('a -> Maybe.maybe 'b) -> set 'a -> set 'b*)
+(*val mapMaybe : forall 'a 'b. SetType 'a, SetType 'b => ('a -> maybe 'b) -> set 'a -> set 'b*)
 val _ = Define `
- ((setMapMaybe:('a -> 'b option) -> 'a set -> 'b set) f s=  
-  (BIGUNION (IMAGE (\ x .  (case f x of 
+ ((setMapMaybe:('a -> 'b option) -> 'a set -> 'b set) f s= 
+   (BIGUNION (IMAGE (\ x .  (case f x of 
                           SOME y  => {y} 
                         | NONE => EMPTY
                         )) s)))`;
 
 
-(*val removeMaybe : forall 'a. SetType 'a => set (Maybe.maybe 'a) -> set 'a*)
+(*val removeMaybe : forall 'a. SetType 'a => set (maybe 'a) -> set 'a*)
 val _ = Define `
  ((removeMaybe:('a option)set -> 'a set) s=  (setMapMaybe (\ x .  x) s))`;
 
@@ -262,15 +262,15 @@ val _ = Define `
 (* min and max              *)
 (* ------------------------ *)
 
-(*val findMin : forall 'a.  SetType 'a, Eq 'a => set 'a -> Maybe.maybe 'a*) 
-(*val findMax : forall 'a.  SetType 'a, Eq 'a => set 'a -> Maybe.maybe 'a*)
+(*val findMin : forall 'a.  SetType 'a, Eq 'a => set 'a -> maybe 'a*) 
+(*val findMax : forall 'a.  SetType 'a, Eq 'a => set 'a -> maybe 'a*)
 
 (* ------------------------ *)
 (* fromList                 *)
 (* ------------------------ *)
 
 (*val fromList : forall 'a.  SetType 'a => list 'a -> set 'a*) (* before from_list *)
-(*val fromListBy : forall 'a.  ('a -> 'a -> Basic_classes.ordering) -> list 'a -> set 'a*) 
+(*val fromListBy : forall 'a.  ('a -> 'a -> ordering) -> list 'a -> set 'a*) 
 
 
 (* ------------------------ *)
@@ -278,7 +278,7 @@ val _ = Define `
 (* ------------------------ *)
 
 (*val sigma : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
-(*val sigmaBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> Basic_classes.ordering) -> set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
+(*val sigmaBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> ('a -> set 'b) -> set ('a * 'b)*)
 
 (*let sigma sa sb=  { (a, b) | forall (a IN sa) (b IN sb a) | true }*)
 
@@ -288,7 +288,7 @@ val _ = Define `
 (* ------------------------ *)
 
 (*val cross : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> set 'b -> set ('a * 'b)*)
-(*val crossBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> Basic_classes.ordering) -> set 'a -> set 'b -> set ('a * 'b)*)
+(*val crossBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> set 'b -> set ('a * 'b)*)
 
 (*let cross s1 s2=  { (e1, e2) | forall (e1 IN s1) (e2 IN s2) | true }*)
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml
index 5409a408..1e51c142 100644
--- a/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml
@@ -44,10 +44,10 @@ val _ = new_theory "lem_set_extra"
  * search criterion, and we avoid baking in the tree representation (although that
  * is the obvious choice).
  *)
-(*val chooseAndSplit : forall 'a. SetType 'a, Ord 'a => set 'a -> Maybe.maybe (set 'a * 'a * set 'a)*)
+(*val chooseAndSplit : forall 'a. SetType 'a, Ord 'a => set 'a -> maybe (set 'a * 'a * set 'a)*)
 val _ = Define `
- ((chooseAndSplit:'a lem_basic_classes$Ord_class -> 'a set ->('a set#'a#'a set)option)dict_Basic_classes_Ord_a s=  
- (if s = EMPTY then
+ ((chooseAndSplit:'a Ord_class -> 'a set ->('a set#'a#'a set)option)dict_Basic_classes_Ord_a s=
+   (if s = EMPTY then
     NONE
   else
     let element1  = (CHOICE s) in
@@ -87,17 +87,17 @@ val _ = Define `
 (* compare                 *)
 (* ----------------------- *)
 
-(*val setCompareBy: forall 'a. ('a -> 'a -> Basic_classes.ordering) -> set 'a -> set 'a -> Basic_classes.ordering*)
+(*val setCompareBy: forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> ordering*)
 val _ = Define `
- ((setCompareBy:('a -> 'a -> lem_basic_classes$ordering) -> 'a set -> 'a set -> lem_basic_classes$ordering) cmp ss ts=  
- (let ss' = (ARB (\ x y .  cmp x y = LT) ss) in
-  let ts' = (ARB (\ x y .  cmp x y = LT) ts) in
+ ((setCompareBy:('a -> 'a -> ordering) -> 'a set -> 'a set -> ordering) cmp ss ts=
+   (let ss' = (ARB (\ x y .  cmp x y = LESS) ss) in
+  let ts' = (ARB (\ x y .  cmp x y = LESS) ts) in
     lexicographic_compare cmp ss' ts'))`;
 
 
-(*val setCompare : forall 'a. SetType 'a, Ord 'a => set 'a -> set 'a -> Basic_classes.ordering*)
+(*val setCompare : forall 'a. SetType 'a, Ord 'a => set 'a -> set 'a -> ordering*)
 val _ = Define `
- ((setCompare:'a lem_basic_classes$Ord_class -> 'a set -> 'a set -> lem_basic_classes$ordering)dict_Basic_classes_Ord_a=  (setCompareBy  
+ ((setCompare:'a Ord_class -> 'a set -> 'a set -> ordering)dict_Basic_classes_Ord_a=  (setCompareBy  
   dict_Basic_classes_Ord_a.compare_method))`;
 
 
@@ -108,8 +108,8 @@ val _ = Define `
 (* Is NOT supported by the coq backend! *)
 (*val leastFixedPointUnbounded : forall 'a. SetType 'a => (set 'a -> set 'a) -> set 'a -> set 'a*)
  val leastFixedPointUnbounded_defn = Hol_defn "leastFixedPointUnbounded" `
- ((leastFixedPointUnbounded:('a set -> 'a set) -> 'a set -> 'a set) f x=   
- (let fx = (f x) in
+ ((leastFixedPointUnbounded:('a set -> 'a set) -> 'a set -> 'a set) f x=
+    (let fx = (f x) in
    if fx SUBSET x then x
    else leastFixedPointUnbounded f (fx UNION x)))`;
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_showScript.sml b/snapshots/hol4/lem/hol-lib/lem_showScript.sml
index 1852c219..eef2c93e 100644
--- a/snapshots/hol4/lem/hol-lib/lem_showScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_showScript.sml
@@ -26,7 +26,7 @@ val _ = Define `
   show_method := (\ s.  STRCAT"\""  (STRCAT s "\""))|>))`;
 
 
-(*val stringFromMaybe : forall 'a. ('a -> string) -> Maybe.maybe 'a -> string*)
+(*val stringFromMaybe : forall 'a. ('a -> string) -> maybe 'a -> string*)
 val _ = Define `
  ((stringFromMaybe:('a -> string) -> 'a option -> string) showX (SOME x)=   (STRCAT"Just ("  (STRCAT(showX x) ")")))
 /\ ((stringFromMaybe:('a -> string) -> 'a option -> string) showX NONE=  "Nothing")`;
@@ -42,8 +42,8 @@ val _ = Define `
 (*val stringFromListAux : forall 'a. ('a -> string) -> list 'a -> string*)
  val stringFromListAux_defn = Defn.Hol_multi_defns `
  ((stringFromListAux:('a -> string) -> 'a list -> string) showX ([])=  "")
-/\ ((stringFromListAux:('a -> string) -> 'a list -> string) showX (x::xs')=      
- ((case xs' of
+/\ ((stringFromListAux:('a -> string) -> 'a list -> string) showX (x::xs')=
+       ((case xs' of
         [] => showX x
       | _ =>  STRCAT(showX x)  (STRCAT"; " (stringFromListAux showX xs'))
       )))`;
@@ -52,8 +52,8 @@ val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn
 
 (*val stringFromList : forall 'a. ('a -> string) -> list 'a -> string*)
 val _ = Define `
- ((stringFromList:('a -> string) -> 'a list -> string) showX xs=   
- (STRCAT"["  (STRCAT(stringFromListAux showX xs) "]")))`;
+ ((stringFromList:('a -> string) -> 'a list -> string) showX xs= 
+   (STRCAT"["  (STRCAT(stringFromListAux showX xs) "]")))`;
 
 
 val _ = Define `
@@ -65,8 +65,8 @@ val _ = Define `
 
 (*val stringFromPair : forall 'a 'b. ('a -> string) -> ('b -> string) -> ('a * 'b) -> string*)
 val _ = Define `
- ((stringFromPair:('a -> string) ->('b -> string) -> 'a#'b -> string) showX showY (x,y)=   
- (STRCAT"("  (STRCAT(showX x)  (STRCAT", "  (STRCAT(showY y) ")")))))`;
+ ((stringFromPair:('a -> string) ->('b -> string) -> 'a#'b -> string) showX showY (x,y)= 
+   (STRCAT"("  (STRCAT(showX x)  (STRCAT", "  (STRCAT(showY y) ")")))))`;
 
 
 val _ = Define `
diff --git a/snapshots/hol4/lem/hol-lib/lem_show_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_show_extraScript.sml
index d8e50e16..6be94271 100644
--- a/snapshots/hol4/lem/hol-lib/lem_show_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_show_extraScript.sml
@@ -14,51 +14,51 @@ val _ = new_theory "lem_show_extra"
 (*import Set_extra String_extra*)
 
 val _ = Define `
-((instance_Show_Show_nat_dict:(num)lem_show$Show_class)= (<|
+((instance_Show_Show_nat_dict:(num)Show_class)= (<|
 
   show_method := num_to_dec_string|>))`;
 
 
 val _ = Define `
-((instance_Show_Show_Num_natural_dict:(num)lem_show$Show_class)= (<|
+((instance_Show_Show_Num_natural_dict:(num)Show_class)= (<|
 
   show_method := num_to_dec_string|>))`;
 
 
 val _ = Define `
-((instance_Show_Show_Num_int_dict:(int)lem_show$Show_class)= (<|
+((instance_Show_Show_Num_int_dict:(int)Show_class)= (<|
 
   show_method := lem_string_extra$stringFromInt|>))`;
 
 
 val _ = Define `
-((instance_Show_Show_Num_integer_dict:(int)lem_show$Show_class)= (<|
+((instance_Show_Show_Num_integer_dict:(int)Show_class)= (<|
 
   show_method := lem_string_extra$stringFromInteger|>))`;
 
 
 val _ = Define `
- ((stringFromSet:('a -> string) -> 'a set -> string) showX xs=   
- (STRCAT"{"  (STRCAT(lem_show$stringFromListAux showX (SET_TO_LIST xs)) "}")))`;
+ ((stringFromSet:('a -> string) -> 'a set -> string) showX xs= 
+   (STRCAT"{"  (STRCAT(lem_show$stringFromListAux showX (SET_TO_LIST xs)) "}")))`;
 
 
 (* Abbreviates the representation if the relation is transitive. *)
 val _ = Define `
- ((stringFromRelation:('a#'a -> string) ->('a#'a)set -> string) showX rel=  
- (if transitive rel then
+ ((stringFromRelation:('a#'a -> string) ->('a#'a)set -> string) showX rel=
+   (if transitive rel then
     let pruned_rel = (withoutTransitiveEdges rel) in
     if (! (e :: rel). (e IN pruned_rel)) then
       (* The relations are the same (there are no transitive edges),
          so we can just as well print the original one. *)
       stringFromSet showX rel
-    else
-       STRCAT"trancl of " (stringFromSet showX pruned_rel)
+    else 
+      STRCAT"trancl of " (stringFromSet showX pruned_rel)
   else
     stringFromSet showX rel))`;
 
 
 val _ = Define `
-((instance_Show_Show_set_dict:'a lem_show$Show_class ->('a set)lem_show$Show_class)dict_Show_Show_a= (<|
+((instance_Show_Show_set_dict:'a Show_class ->('a set)Show_class)dict_Show_Show_a= (<|
 
   show_method := (\ xs. stringFromSet  
   dict_Show_Show_a.show_method xs)|>))`;
diff --git a/snapshots/hol4/lem/hol-lib/lem_sortingScript.sml b/snapshots/hol4/lem/hol-lib/lem_sortingScript.sml
index 30f66e5e..08288d15 100644
--- a/snapshots/hol4/lem/hol-lib/lem_sortingScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_sortingScript.sml
@@ -90,15 +90,15 @@ val _ = Define `
 
 (*val sort: forall 'a. Ord 'a => list 'a -> list 'a*)
 (*val sortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
-(*val sortByOrd: forall 'a. ('a -> 'a -> Basic_classes.ordering) -> list 'a -> list 'a*)
+(*val sortByOrd: forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a*)
 
-(*val predicate_of_ord : forall 'a. ('a -> 'a -> Basic_classes.ordering) -> 'a -> 'a -> bool*)
+(*val predicate_of_ord : forall 'a. ('a -> 'a -> ordering) -> 'a -> 'a -> bool*)
 val _ = Define `
- ((predicate_of_ord:('a -> 'a -> lem_basic_classes$ordering) -> 'a -> 'a -> bool) f x y=  
- ((case f x y of
-      LT => T
-    | EQ => T
-    | GT => F
+ ((predicate_of_ord:('a -> 'a -> ordering) -> 'a -> 'a -> bool) f x y=
+   ((case f x y of
+      LESS => T
+    | EQUAL => T
+    | GREATER => F
   )))`;
 
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_stringScript.sml b/snapshots/hol4/lem/hol-lib/lem_stringScript.sml
index 9dd53778..f91a4cb0 100644
--- a/snapshots/hol4/lem/hol-lib/lem_stringScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_stringScript.sml
@@ -50,8 +50,8 @@ val _ = new_theory "lem_string"
 
 (*val string_case : forall 'a. string -> 'a -> (char -> string -> 'a) -> 'a*)
 
-(*let string_case s c_empty c_cons= 
-  match (toCharList s) with
+(*let string_case s c_empty c_cons=
+   match (toCharList s) with
     | [] -> c_empty
     | c :: cs -> c_cons c (toString cs)
   end*)
@@ -63,8 +63,8 @@ val _ = new_theory "lem_string"
 (*val concat : string -> list string -> string*)
  val concat_defn = Defn.Hol_multi_defns `
  ((concat:string ->(string)list -> string) sep ([])=  "")
-/\ ((concat:string ->(string)list -> string) sep (s :: ss')=      
- ((case ss' of
+/\ ((concat:string ->(string)list -> string) sep (s :: ss')=
+       ((case ss' of
         [] => s
       | _ =>  STRCAT s  (STRCAT sep (concat sep ss'))
       )))`;
diff --git a/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml
index 0801601a..33f71ab7 100644
--- a/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml
@@ -35,8 +35,8 @@ val _ = new_theory "lem_string_extra"
 
 (*val stringFromNatHelper : nat -> list char -> list char*)
  val stringFromNatHelper_defn = Hol_defn "stringFromNatHelper" `
- ((stringFromNatHelper:num ->(char)list ->(char)list) n acc=  
- (if n =( 0 : num) then
+ ((stringFromNatHelper:num ->(char)list ->(char)list) n acc=
+   (if n =( 0 : num) then
     acc
   else
     stringFromNatHelper (n DIV( 10 : num)) (CHR ((n MOD( 10 : num)) +( 48 : num)) :: acc)))`;
@@ -45,32 +45,32 @@ val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn
 
 (*val stringFromNat : nat -> string*)
 
-(*val stringFromNaturalHelper : Num.natural -> list char -> list char*)
+(*val stringFromNaturalHelper : natural -> list char -> list char*)
  val stringFromNaturalHelper_defn = Hol_defn "stringFromNaturalHelper" `
- ((stringFromNaturalHelper:num ->(char)list ->(char)list) n acc=  
- (if n =( 0:num) then
+ ((stringFromNaturalHelper:num ->(char)list ->(char)list) n acc=
+   (if n =( 0:num) then
     acc
   else
     stringFromNaturalHelper (n DIV( 10:num)) (CHR ((((n MOD( 10:num)) +( 48:num)):num)) :: acc)))`;
 
 val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNaturalHelper_defn;
 
-(*val stringFromNatural : Num.natural -> string*)
+(*val stringFromNatural : natural -> string*)
 
-(*val stringFromInt : Num.int -> string*)
+(*val stringFromInt : int -> string*)
 val _ = Define `
- ((stringFromInt:int -> string) i=  
-  (if i <( 0 : int) then 
-     STRCAT"-" (num_to_dec_string (Num (ABS i)))
+ ((stringFromInt:int -> string) i= 
+   (if i <( 0 : int) then  
+    STRCAT"-" (num_to_dec_string (Num (ABS i)))
   else
     num_to_dec_string (Num (ABS i))))`;
 
 
-(*val stringFromInteger : Num.integer -> string*)
+(*val stringFromInteger : integer -> string*)
 val _ = Define `
- ((stringFromInteger:int -> string) i=  
-  (if i <( 0 : int) then 
-     STRCAT"-" (num_to_dec_string (Num (ABS i)))
+ ((stringFromInteger:int -> string) i= 
+   (if i <( 0 : int) then  
+    STRCAT"-" (num_to_dec_string (Num (ABS i)))
   else
     num_to_dec_string (Num (ABS i))))`;
 
@@ -84,20 +84,20 @@ val _ = Define `
 (*let nth s n=  List_extra.nth (toCharList s) n*)
 
 (*val stringConcat : list string -> string*)
-(*let stringConcat s= 
-  List.foldr (^) "" s*)
+(*let stringConcat s=
+   List.foldr (^) "" s*)
 
 (******************************************************************************)
 (* String comparison                                                          *)
 (******************************************************************************)
 
-(*val stringCompare : string -> string -> Basic_classes.ordering*)
+(*val stringCompare : string -> string -> ordering*)
 
 val _ = Define `
- ((stringLess:string -> string -> bool) x y=  (orderingIsLess (EQ)))`;
+ ((stringLess:string -> string -> bool) x y=  (orderingIsLess (EQUAL)))`;
 
 val _ = Define `
- ((stringLessEq:string -> string -> bool) x y=  (~ (orderingIsGreater (EQ))))`;
+ ((stringLessEq:string -> string -> bool) x y=  (~ (orderingIsGreater (EQUAL))))`;
 
 val _ = Define `
  ((stringGreater:string -> string -> bool) x y=  (stringLess y x))`;
@@ -107,9 +107,9 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Basic_classes_Ord_string_dict:(string)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_string_dict:(string)Ord_class)= (<|
 
-  compare_method := (\ x y. EQ);
+  compare_method := (\ x y. EQUAL);
 
   isLess_method := stringLess;
 
diff --git a/snapshots/hol4/lem/hol-lib/lem_wordScript.sml b/snapshots/hol4/lem/hol-lib/lem_wordScript.sml
index 690909a0..a8639e81 100644
--- a/snapshots/hol4/lem/hol-lib/lem_wordScript.sml
+++ b/snapshots/hol4/lem/hol-lib/lem_wordScript.sml
@@ -32,8 +32,8 @@ val _ = Hol_datatype `
 (*val boolListFrombitSeq : nat -> bitSequence -> list bool*)
 
  val _ = Define `
- ((boolListFrombitSeqAux:num -> 'a -> 'a list -> 'a list) n s bl=  
- (if n =( 0 : num) then [] else
+ ((boolListFrombitSeqAux:num -> 'a -> 'a list -> 'a list) n s bl=
+   (if n =( 0 : num) then [] else
   (case bl of
       []       => REPLICATE n s
     | b :: bl' => b :: (boolListFrombitSeqAux (n -( 1 : num)) s bl')
@@ -45,10 +45,10 @@ val _ = Define `
 
 
 
-(*val bitSeqFromBoolList : list bool -> Maybe.maybe bitSequence*)
+(*val bitSeqFromBoolList : list bool -> maybe bitSequence*)
 val _ = Define `
- ((bitSeqFromBoolList:(bool)list ->(bitSequence)option) bl=  
- ((case dest_init bl of
+ ((bitSeqFromBoolList:(bool)list ->(bitSequence)option) bl=
+   ((case dest_init bl of
       NONE => NONE
     | SOME (bl', s) => SOME (BitSeq (SOME (LENGTH bl)) s bl')
   )))`;
@@ -65,7 +65,7 @@ val _ = Define `
 
 
 
-(*val bitSeqTestBit : bitSequence -> nat -> Maybe.maybe bool*)
+(*val bitSeqTestBit : bitSequence -> nat -> maybe bool*)
 val _ = Define `
  ((bitSeqTestBit:bitSequence -> num ->(bool)option) (BitSeq NONE s bl) pos=  (if pos < LENGTH bl then list_index bl pos else SOME s))
 /\ ((bitSeqTestBit:bitSequence -> num ->(bool)option) (BitSeq(SOME l) s bl) pos=  (if (pos >= l) then NONE else
@@ -75,15 +75,15 @@ val _ = Define `
 
 (*val bitSeqSetBit : bitSequence -> nat -> bool -> bitSequence*)
 val _ = Define `
- ((bitSeqSetBit:bitSequence -> num -> bool -> bitSequence) (BitSeq len s bl) pos v=  
- (let bl' = (if (pos < LENGTH bl) then bl else bl ++ REPLICATE pos s) in
+ ((bitSeqSetBit:bitSequence -> num -> bool -> bitSequence) (BitSeq len s bl) pos v=
+   (let bl' = (if (pos < LENGTH bl) then bl else bl ++ REPLICATE pos s) in
   let bl'' = (LUPDATE v pos bl') in
   let bs' = (BitSeq len s bl'') in
   cleanBitSeq bs'))`;
 
 
 
-(*val resizeBitSeq : Maybe.maybe nat -> bitSequence -> bitSequence*)
+(*val resizeBitSeq : maybe nat -> bitSequence -> bitSequence*)
 val _ = Define `
  ((resizeBitSeq:(num)option -> bitSequence -> bitSequence) new_len bs= 
   ((case cleanBitSeq bs of
@@ -165,8 +165,8 @@ val _ = Define `
 
 (*val bitSeqLogicalShiftRight : bitSequence -> nat -> bitSequence*)
 val _ = Define `
- ((bitSeqLogicalShiftRight:bitSequence -> num -> bitSequence) bs n=  
-  (if (n =( 0 : num)) then cleanBitSeq bs else  
+ ((bitSeqLogicalShiftRight:bitSequence -> num -> bitSequence) bs n= 
+   (if (n =( 0 : num)) then cleanBitSeq bs else  
   (case cleanBitSeq bs of
       (BitSeq len s bl) =>
   (case len of
@@ -180,7 +180,7 @@ val _ = Define `
 (* integerFromBoolList sign bl creates an integer from a list of bits
    (least significant bit first) and an explicitly given sign bit.
    It uses two's complement encoding. *)
-(*val integerFromBoolList : (bool * list bool) -> Num.integer*)
+(*val integerFromBoolList : (bool * list bool) -> integer*)
 
  val _ = Define `
  ((integerFromBoolListAux:int ->(bool)list -> int) (acc : int) (([]) : bool list)=  acc)
@@ -189,18 +189,18 @@ val _ = Define `
 
 
 val _ = Define `
- ((integerFromBoolList:bool#(bool)list -> int) (sign, bl)=   
-  (if sign then 
+ ((integerFromBoolList:bool#(bool)list -> int) (sign, bl)= 
+    (if sign then 
      ~ (integerFromBoolListAux(( 0 : int)) (REVERSE (MAP (\ x. ~ x) bl)) +( 1 : int))
    else integerFromBoolListAux(( 0 : int)) (REVERSE bl)))`;
 
 
 (* [boolListFromInteger i] creates a sign bit and a list of booleans from an integer. The len_opt tells it when to stop.*)
-(*val boolListFromInteger :    Num.integer -> bool * list bool*)
+(*val boolListFromInteger :    integer -> bool * list bool*)
 
  val _ = Define `
- ((boolListFromNatural:(bool)list -> num ->(bool)list) acc (remainder : num)= 
- (if (remainder >( 0:num)) then 
+ ((boolListFromNatural:(bool)list -> num ->(bool)list) acc (remainder : num)=
+  (if (remainder >( 0:num)) then 
    (boolListFromNatural (((remainder MOD( 2:num)) =( 1:num)) :: acc) 
       (remainder DIV( 2:num)))
  else
@@ -208,8 +208,8 @@ val _ = Define `
 
 
 val _ = Define `
- ((boolListFromInteger:int -> bool#(bool)list) (i : int)=  
-  (if (i <( 0 : int)) then
+ ((boolListFromInteger:int -> bool#(bool)list) (i : int)= 
+   (if (i <( 0 : int)) then
     (T, MAP (\ x. ~ x) (boolListFromNatural [] (Num (ABS (~ (i +( 1 : int)))))))
   else
     (F, boolListFromNatural [] (Num (ABS i)))))`;
@@ -218,15 +218,15 @@ val _ = Define `
 
 (* [bitSeqFromInteger len_opt i] encodes [i] as a bitsequence with [len_opt] bits. If there are not enough
    bits, truncation happens *)
-(*val bitSeqFromInteger : Maybe.maybe nat -> Num.integer -> bitSequence*)
+(*val bitSeqFromInteger : maybe nat -> integer -> bitSequence*)
 val _ = Define `
- ((bitSeqFromInteger:(num)option -> int -> bitSequence) len_opt i=  
- (let (s, bl) = (boolListFromInteger i) in
+ ((bitSeqFromInteger:(num)option -> int -> bitSequence) len_opt i=
+   (let (s, bl) = (boolListFromInteger i) in
   resizeBitSeq len_opt (BitSeq NONE s bl)))`;
 
 
 
-(*val integerFromBitSeq : bitSequence -> Num.integer*)
+(*val integerFromBitSeq : bitSequence -> integer*)
 val _ = Define `
  ((integerFromBitSeq:bitSequence -> int) bs= 
   ((case cleanBitSeq bs of (BitSeq len s bl) => integerFromBoolList (s, bl) )))`;
@@ -235,7 +235,7 @@ val _ = Define `
 
 (* Now we can via translation to integers map arithmetic operations to bitSequences *)
 
-(*val bitSeqArithUnaryOp : (Num.integer -> Num.integer) -> bitSequence -> bitSequence*)
+(*val bitSeqArithUnaryOp : (integer -> integer) -> bitSequence -> bitSequence*)
 val _ = Define `
  ((bitSeqArithUnaryOp:(int -> int) -> bitSequence -> bitSequence) uop bs= 
   ((case bs of
@@ -244,7 +244,7 @@ val _ = Define `
    )))`;
 
 
-(*val bitSeqArithBinOp : (Num.integer -> Num.integer -> Num.integer) -> bitSequence -> bitSequence -> bitSequence*)
+(*val bitSeqArithBinOp : (integer -> integer -> integer) -> bitSequence -> bitSequence -> bitSequence*)
 val _ = Define `
  ((bitSeqArithBinOp:(int -> int -> int) -> bitSequence -> bitSequence -> bitSequence) binop bs1 bs2= 
   ((case bs1 of
@@ -261,7 +261,7 @@ val _ = Define `
    )))`;
 
 
-(*val bitSeqArithBinTest : forall 'a. (Num.integer -> Num.integer -> 'a) -> bitSequence -> bitSequence -> 'a*)
+(*val bitSeqArithBinTest : forall 'a. (integer -> integer -> 'a) -> bitSequence -> bitSequence -> 'a*)
 val _ = Define `
  ((bitSeqArithBinTest:(int -> int -> 'a) -> bitSequence -> bitSequence -> 'a) binop bs1 bs2=  (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2)))`;
 
@@ -291,13 +291,13 @@ val _ = Define `
  ((bitSeqGreaterEqual:bitSequence -> bitSequence -> bool) bs1 bs2=  (bitSeqArithBinTest (>=) bs1 bs2))`;
 
 
-(*val bitSeqCompare : bitSequence -> bitSequence -> Basic_classes.ordering*)
+(*val bitSeqCompare : bitSequence -> bitSequence -> ordering*)
 val _ = Define `
- ((bitSeqCompare:bitSequence -> bitSequence -> lem_basic_classes$ordering) bs1 bs2=  (bitSeqArithBinTest (genericCompare (<) (=)) bs1 bs2))`;
+ ((bitSeqCompare:bitSequence -> bitSequence -> ordering) bs1 bs2=  (bitSeqArithBinTest (genericCompare (<) (=)) bs1 bs2))`;
 
 
 val _ = Define `
-((instance_Basic_classes_Ord_Word_bitSequence_dict:(bitSequence)lem_basic_classes$Ord_class)= (<|
+((instance_Basic_classes_Ord_Word_bitSequence_dict:(bitSequence)Ord_class)= (<|
 
   compare_method := bitSeqCompare;
 
@@ -317,7 +317,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumNegate_Word_bitSequence_dict:(bitSequence)lem_num$NumNegate_class)= (<|
+((instance_Num_NumNegate_Word_bitSequence_dict:(bitSequence)NumNegate_class)= (<|
 
   numNegate_method := bitSeqNegate|>))`;
 
@@ -329,7 +329,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumAdd_Word_bitSequence_dict:(bitSequence)lem_num$NumAdd_class)= (<|
+((instance_Num_NumAdd_Word_bitSequence_dict:(bitSequence)NumAdd_class)= (<|
 
   numAdd_method := bitSeqAdd|>))`;
 
@@ -340,7 +340,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumMinus_Word_bitSequence_dict:(bitSequence)lem_num$NumMinus_class)= (<|
+((instance_Num_NumMinus_Word_bitSequence_dict:(bitSequence)NumMinus_class)= (<|
 
   numMinus_method := bitSeqMinus|>))`;
 
@@ -351,7 +351,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumSucc_Word_bitSequence_dict:(bitSequence)lem_num$NumSucc_class)= (<|
+((instance_Num_NumSucc_Word_bitSequence_dict:(bitSequence)NumSucc_class)= (<|
 
   succ_method := bitSeqSucc|>))`;
 
@@ -362,7 +362,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumPred_Word_bitSequence_dict:(bitSequence)lem_num$NumPred_class)= (<|
+((instance_Num_NumPred_Word_bitSequence_dict:(bitSequence)NumPred_class)= (<|
 
   pred_method := bitSeqPred|>))`;
 
@@ -373,7 +373,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumMult_Word_bitSequence_dict:(bitSequence)lem_num$NumMult_class)= (<|
+((instance_Num_NumMult_Word_bitSequence_dict:(bitSequence)NumMult_class)= (<|
 
   numMult_method := bitSeqMult|>))`;
 
@@ -385,7 +385,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumPow_Word_bitSequence_dict:(bitSequence)lem_num$NumPow_class)= (<|
+((instance_Num_NumPow_Word_bitSequence_dict:(bitSequence)NumPow_class)= (<|
 
   numPow_method := bitSeqPow|>))`;
 
@@ -396,13 +396,13 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumIntegerDivision_Word_bitSequence_dict:(bitSequence)lem_num$NumIntegerDivision_class)= (<|
+((instance_Num_NumIntegerDivision_Word_bitSequence_dict:(bitSequence)NumIntegerDivision_class)= (<|
 
   div_method := bitSeqDiv|>))`;
 
 
 val _ = Define `
-((instance_Num_NumDivision_Word_bitSequence_dict:(bitSequence)lem_num$NumDivision_class)= (<|
+((instance_Num_NumDivision_Word_bitSequence_dict:(bitSequence)NumDivision_class)= (<|
 
   numDivision_method := bitSeqDiv|>))`;
 
@@ -413,7 +413,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Num_NumRemainder_Word_bitSequence_dict:(bitSequence)lem_num$NumRemainder_class)= (<|
+((instance_Num_NumRemainder_Word_bitSequence_dict:(bitSequence)NumRemainder_class)= (<|
 
   mod_method := bitSeqMod|>))`;
 
@@ -429,7 +429,7 @@ val _ = Define `
 
 
 val _ = Define `
-((instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict:(bitSequence)lem_basic_classes$OrdMaxMin_class)= (<|
+((instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict:(bitSequence)OrdMaxMin_class)= (<|
 
   max_method := bitSeqMax;
 
@@ -537,7 +537,7 @@ val _ = Define `
 (* int32                   *)
 (* ----------------------- *)
 
-(*val int32Lnot : Num.int32 -> Num.int32*) (* XXX: fix *)
+(*val int32Lnot : int32 -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordNot_Num_int32_dict:(word32)WordNot_class)= (<|
@@ -546,7 +546,7 @@ val _ = Define `
 
 
 
-(*val int32Lor  : Num.int32 -> Num.int32 -> Num.int32*) (* XXX: fix *)
+(*val int32Lor  : int32 -> int32 -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordOr_Num_int32_dict:(word32)WordOr_class)= (<|
@@ -554,7 +554,7 @@ val _ = Define `
   lor_method := word_or|>))`;
 
 
-(*val int32Lxor : Num.int32 -> Num.int32 -> Num.int32*) (* XXX: fix *)
+(*val int32Lxor : int32 -> int32 -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordXor_Num_int32_dict:(word32)WordXor_class)= (<|
@@ -562,7 +562,7 @@ val _ = Define `
   lxor_method := word_xor|>))`;
 
 
-(*val int32Land : Num.int32 -> Num.int32 -> Num.int32*) (* XXX: fix *)
+(*val int32Land : int32 -> int32 -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordAnd_Num_int32_dict:(word32)WordAnd_class)= (<|
@@ -570,7 +570,7 @@ val _ = Define `
   land_method := word_and|>))`;
 
 
-(*val int32Lsl  : Num.int32 -> nat -> Num.int32*) (* XXX: fix *)
+(*val int32Lsl  : int32 -> nat -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordLsl_Num_int32_dict:(word32)WordLsl_class)= (<|
@@ -578,7 +578,7 @@ val _ = Define `
   lsl_method := word_lsl|>))`;
 
 
-(*val int32Lsr  : Num.int32 -> nat -> Num.int32*) (* XXX: fix *)
+(*val int32Lsr  : int32 -> nat -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordLsr_Num_int32_dict:(word32)WordLsr_class)= (<|
@@ -587,7 +587,7 @@ val _ = Define `
 
 
 
-(*val int32Asr  : Num.int32 -> nat -> Num.int32*) (* XXX: fix *)
+(*val int32Asr  : int32 -> nat -> int32*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordAsr_Num_int32_dict:(word32)WordAsr_class)= (<|
@@ -600,7 +600,7 @@ val _ = Define `
 (* int64                   *)
 (* ----------------------- *)
 
-(*val int64Lnot : Num.int64 -> Num.int64*) (* XXX: fix *)
+(*val int64Lnot : int64 -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordNot_Num_int64_dict:(word64)WordNot_class)= (<|
@@ -608,7 +608,7 @@ val _ = Define `
   lnot_method := (\ w. (~ w))|>))`;
 
 
-(*val int64Lor  : Num.int64 -> Num.int64 -> Num.int64*) (* XXX: fix *)
+(*val int64Lor  : int64 -> int64 -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordOr_Num_int64_dict:(word64)WordOr_class)= (<|
@@ -616,7 +616,7 @@ val _ = Define `
   lor_method := word_or|>))`;
 
 
-(*val int64Lxor : Num.int64 -> Num.int64 -> Num.int64*) (* XXX: fix *)
+(*val int64Lxor : int64 -> int64 -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordXor_Num_int64_dict:(word64)WordXor_class)= (<|
@@ -624,7 +624,7 @@ val _ = Define `
   lxor_method := word_xor|>))`;
 
 
-(*val int64Land : Num.int64 -> Num.int64 -> Num.int64*) (* XXX: fix *)
+(*val int64Land : int64 -> int64 -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordAnd_Num_int64_dict:(word64)WordAnd_class)= (<|
@@ -632,7 +632,7 @@ val _ = Define `
   land_method := word_and|>))`;
 
 
-(*val int64Lsl  : Num.int64 -> nat -> Num.int64*) (* XXX: fix *)
+(*val int64Lsl  : int64 -> nat -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordLsl_Num_int64_dict:(word64)WordLsl_class)= (<|
@@ -640,7 +640,7 @@ val _ = Define `
   lsl_method := word_lsl|>))`;
 
 
-(*val int64Lsr  : Num.int64 -> nat -> Num.int64*) (* XXX: fix *)
+(*val int64Lsr  : int64 -> nat -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordLsr_Num_int64_dict:(word64)WordLsr_class)= (<|
@@ -648,7 +648,7 @@ val _ = Define `
   lsr_method := word_lsr|>))`;
 
 
-(*val int64Asr  : Num.int64 -> nat -> Num.int64*) (* XXX: fix *)
+(*val int64Asr  : int64 -> nat -> int64*) (* XXX: fix *)
 
 val _ = Define `
 ((instance_Word_WordAsr_Num_int64_dict:(word64)WordAsr_class)= (<|
@@ -700,7 +700,7 @@ val _ = Define `
 (* integer                 *)
 (* ----------------------- *)
 
-(*val integerLnot : Num.integer -> Num.integer*)
+(*val integerLnot : integer -> integer*)
 val _ = Define `
  ((integerLnot:int -> int) i=  (~ (i +( 1 : int))))`;
 
@@ -712,7 +712,7 @@ val _ = Define `
 
 
 
-(*val integerLor  : Num.integer -> Num.integer -> Num.integer*)
+(*val integerLor  : integer -> integer -> integer*)
 val _ = Define `
  ((integerLor:int -> int -> int) i1 i2=  (defaultLor integerFromBitSeq (bitSeqFromInteger NONE) i1 i2))`;
 
@@ -723,7 +723,7 @@ val _ = Define `
   lor_method := integerLor|>))`;
 
 
-(*val integerLxor : Num.integer -> Num.integer -> Num.integer*)
+(*val integerLxor : integer -> integer -> integer*)
 val _ = Define `
  ((integerLxor:int -> int -> int) i1 i2=  (defaultLxor integerFromBitSeq (bitSeqFromInteger NONE) i1 i2))`;
 
@@ -734,7 +734,7 @@ val _ = Define `
   lxor_method := integerLxor|>))`;
 
 
-(*val integerLand : Num.integer -> Num.integer -> Num.integer*)
+(*val integerLand : integer -> integer -> integer*)
 val _ = Define `
  ((integerLand:int -> int -> int) i1 i2=  (defaultLand integerFromBitSeq (bitSeqFromInteger NONE) i1 i2))`;
 
@@ -745,7 +745,7 @@ val _ = Define `
   land_method := integerLand|>))`;
 
 
-(*val integerLsl  : Num.integer -> nat -> Num.integer*)
+(*val integerLsl  : integer -> nat -> integer*)
 val _ = Define `
  ((integerLsl:int -> num -> int) i n=  (defaultLsl integerFromBitSeq (bitSeqFromInteger NONE) i n))`;
 
@@ -756,7 +756,7 @@ val _ = Define `
   lsl_method := integerLsl|>))`;
 
 
-(*val integerAsr  : Num.integer -> nat -> Num.integer*)
+(*val integerAsr  : integer -> nat -> integer*)
 val _ = Define `
  ((integerAsr:int -> num -> int) i n=  (defaultAsr integerFromBitSeq (bitSeqFromInteger NONE) i n))`;
 
@@ -783,19 +783,19 @@ val _ = Define `
    it should be used very carefully and only for operations that don't depend on the
    bitwidth of int *)
 
-(*val intFromBitSeq : bitSequence -> Num.int*)
+(*val intFromBitSeq : bitSequence -> int*)
 val _ = Define `
  ((intFromBitSeq:bitSequence -> int) bs=  (I (integerFromBitSeq (resizeBitSeq (SOME(( 31 : num))) bs))))`;
 
 
 
-(*val bitSeqFromInt : Num.int -> bitSequence*) 
+(*val bitSeqFromInt : int -> bitSequence*) 
 val _ = Define `
  ((bitSeqFromInt:int -> bitSequence) i=  (bitSeqFromInteger (SOME(( 31 : num))) ( i)))`;
 
 
 
-(*val intLnot : Num.int -> Num.int*)
+(*val intLnot : int -> int*)
 val _ = Define `
  ((intLnot:int -> int) i=  (~ (i +( 1 : int))))`;
 
@@ -806,7 +806,7 @@ val _ = Define `
   lnot_method := intLnot|>))`;
 
 
-(*val intLor  : Num.int -> Num.int -> Num.int*)
+(*val intLor  : int -> int -> int*)
 val _ = Define `
  ((intLor:int -> int -> int) i1 i2=  (defaultLor intFromBitSeq bitSeqFromInt i1 i2))`;
 
@@ -817,7 +817,7 @@ val _ = Define `
   lor_method := intLor|>))`;
 
 
-(*val intLxor : Num.int -> Num.int -> Num.int*)
+(*val intLxor : int -> int -> int*)
 val _ = Define `
  ((intLxor:int -> int -> int) i1 i2=  (defaultLxor intFromBitSeq bitSeqFromInt i1 i2))`;
 
@@ -828,7 +828,7 @@ val _ = Define `
   lxor_method := intLxor|>))`;
 
 
-(*val intLand : Num.int -> Num.int -> Num.int*)
+(*val intLand : int -> int -> int*)
 val _ = Define `
  ((intLand:int -> int -> int) i1 i2=  (defaultLand intFromBitSeq bitSeqFromInt i1 i2))`;
 
@@ -839,7 +839,7 @@ val _ = Define `
   land_method := intLand|>))`;
 
 
-(*val intLsl  : Num.int -> nat -> Num.int*)
+(*val intLsl  : int -> nat -> int*)
 val _ = Define `
  ((intLsl:int -> num -> int) i n=  (defaultLsl intFromBitSeq bitSeqFromInt i n))`;
 
@@ -850,7 +850,7 @@ val _ = Define `
   lsl_method := intLsl|>))`;
 
 
-(*val intAsr  : Num.int -> nat -> Num.int*)
+(*val intAsr  : int -> nat -> int*)
 val _ = Define `
  ((intAsr:int -> num -> int) i n=  (defaultAsr intFromBitSeq bitSeqFromInt i n))`;
 
@@ -869,17 +869,17 @@ val _ = Define `
 
 (* some operations work also on positive numbers *)
 
-(*val naturalFromBitSeq : bitSequence -> Num.natural*)
+(*val naturalFromBitSeq : bitSequence -> natural*)
 val _ = Define `
  ((naturalFromBitSeq:bitSequence -> num) bs=  (Num (ABS (integerFromBitSeq bs))))`;
 
 
-(*val bitSeqFromNatural : Maybe.maybe nat -> Num.natural -> bitSequence*)
+(*val bitSeqFromNatural : maybe nat -> natural -> bitSequence*)
 val _ = Define `
  ((bitSeqFromNatural:(num)option -> num -> bitSequence) len n=  (bitSeqFromInteger len (int_of_num n)))`;
 
 
-(*val naturalLor  : Num.natural -> Num.natural -> Num.natural*)
+(*val naturalLor  : natural -> natural -> natural*)
 val _ = Define `
  ((naturalLor:num -> num -> num) i1 i2=  (defaultLor naturalFromBitSeq (bitSeqFromNatural NONE) i1 i2))`;
 
@@ -890,7 +890,7 @@ val _ = Define `
   lor_method := naturalLor|>))`;
 
 
-(*val naturalLxor : Num.natural -> Num.natural -> Num.natural*)
+(*val naturalLxor : natural -> natural -> natural*)
 val _ = Define `
  ((naturalLxor:num -> num -> num) i1 i2=  (defaultLxor naturalFromBitSeq (bitSeqFromNatural NONE) i1 i2))`;
 
@@ -901,7 +901,7 @@ val _ = Define `
   lxor_method := naturalLxor|>))`;
 
 
-(*val naturalLand : Num.natural -> Num.natural -> Num.natural*)
+(*val naturalLand : natural -> natural -> natural*)
 val _ = Define `
  ((naturalLand:num -> num -> num) i1 i2=  (defaultLand naturalFromBitSeq (bitSeqFromNatural NONE) i1 i2))`;
 
@@ -912,7 +912,7 @@ val _ = Define `
   land_method := naturalLand|>))`;
 
 
-(*val naturalLsl  : Num.natural -> nat -> Num.natural*)
+(*val naturalLsl  : natural -> nat -> natural*)
 val _ = Define `
  ((naturalLsl:num -> num -> num) i n=  (defaultLsl naturalFromBitSeq (bitSeqFromNatural NONE) i n))`;
 
@@ -923,7 +923,7 @@ val _ = Define `
   lsl_method := naturalLsl|>))`;
 
 
-(*val naturalAsr  : Num.natural -> nat -> Num.natural*)
+(*val naturalAsr  : natural -> nat -> natural*)
 val _ = Define `
  ((naturalAsr:num -> num -> num) i n=  (defaultAsr naturalFromBitSeq (bitSeqFromNatural NONE) i n))`;