diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/rule-def.sml
--- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -10,19 +10,21 @@
   type calc
   eqtype calID
   eqtype errpatID
-  type rew_ord' = string
-  type rew_ord_ = LibraryC.subst -> term * term -> bool
-  type rew_ord = rew_ord' * rew_ord_
+
+  type rew_ord_id = string
+  type rew_ord_function = LibraryC.subst -> term * term -> bool
+  type rew_ord_T = rew_ord_id * rew_ord_function
+
   type eval_fn = string -> term -> Proof.context -> (string * term) option
 
   datatype rule_set =
        Empty
      | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
-       preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
+       preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
      | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
-       preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
+       preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
      | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
-       prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
+       prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program}
   and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule
      | Rls_ of rule_set | Thm of string * thm
   and program =
@@ -44,9 +46,9 @@
 
 type eval_fn = string -> term -> Proof.context -> (string * term) option;
 
-type rew_ord' = string;
-type rew_ord_ = LibraryC.subst -> term * term -> bool;
-type rew_ord = rew_ord' * rew_ord_;
+type rew_ord_id = string;
+type rew_ord_function = LibraryC.subst -> term * term -> bool;
+type rew_ord_T = rew_ord_id * rew_ord_function;
 
 type calID = string;
 type cal = calID * eval_fn;
@@ -109,7 +111,7 @@
   | Repeat of         (*a confluent and terminating ruleset, in principle             *)
     {id: string,      (* for trace_rewrite                                            *)
      preconds: term list, (* STILL UNUSED                                             *)
-     rew_ord: rew_ord,(* for rules                                                    *)                                             
+     rew_ord: rew_ord_T,(* for rules                                                  *)                                             
      erls: rule_set,  (* for the conditions in rules                                  *)
      srls: rule_set,  (* for evaluation of Prog_Expr                                  *)
      calc: calc list, (* for Calculate in program, set by prep_rls'                   *)
@@ -117,7 +119,7 @@
      errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy              *)
      scr: program}    (* DEPRECATED: intersteps are created on the fly now            *)
   | Sequence of       (* a sequence of rules to be tried only once                    *)
-    {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
+    {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set,
      calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
   | Rrls of           (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
     {id: string,      (* for trace_rewrite                                            *)
@@ -125,7 +127,7 @@
        (term list *   (* preconds, eval with subst from pattern below                 *)
 		     term)        (* pattern matched with current (sub)term                       *)
 		   list,          (* meta-conjunction in guarding is or                           *)
-     rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
+     rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
 
 fun program_to_string Empty_Prog = "Empty_Prog"
   | program_to_string (Prog s) = "Prog " ^ UnparseC.term s