diff -r 3b194392ea71 -r bb153a08645b src/Tools/isac/MathEngBasic/tactic.sml
--- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 15:02:50 2020 +0200
+++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 10 16:16:09 2020 +0200
@@ -77,9 +77,9 @@
   | Check_elementwise of TermC.as_string
   | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
 
-  | Derive of Rule_Set.identifier
-  | Detail_Set of Rule_Set.identifier
-  | Detail_Set_Inst of Selem.subs * Rule_Set.identifier
+  | Derive of Rule_Set.id
+  | Detail_Set of Rule_Set.id
+  | Detail_Set_Inst of Selem.subs * Rule_Set.id
   | End_Detail
 
   | Empty_Tac
@@ -93,8 +93,8 @@
 
   | Rewrite of ThmC_Def.thm''
   | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
-  | Rewrite_Set of Rule_Set.identifier
-  | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
+  | Rewrite_Set of Rule_Set.id
+  | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
 
   | Specify_Method of Celem.metID
   | Specify_Problem of Celem.pblID
@@ -111,7 +111,7 @@
   val eq_tac : input * input -> bool
   val is_rewtac : input -> bool
   val is_rewset : input -> bool
-  val rls_of : input -> Rule_Set.identifier
+  val rls_of : input -> Rule_Set.id
   val rule2tac : theory -> (term * term) list ->  Rule.rule -> input
   val input_from_T : T -> input
   val result : T -> term
@@ -165,9 +165,9 @@
   | Check_elementwise of TermC.as_string
   | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
 
-  | Derive of Rule_Set.identifier                 (* WN0509 drop *)
-  | Detail_Set of Rule_Set.identifier             (* WN0509 drop *)
-  | Detail_Set_Inst of Selem.subs * Rule_Set.identifier (* WN0509 drop *)
+  | Derive of Rule_Set.id                 (* WN0509 drop *)
+  | Detail_Set of Rule_Set.id             (* WN0509 drop *)
+  | Detail_Set_Inst of Selem.subs * Rule_Set.id (* WN0509 drop *)
   | End_Detail                     (* WN0509 drop *)
 
   | Empty_Tac
@@ -185,8 +185,8 @@
      and thm is created from ThmID by assoc_thm'' when entering isabisac *)
   | Rewrite of ThmC_Def.thm''
   | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
-  | Rewrite_Set of Rule_Set.identifier
-  | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
+  | Rewrite_Set of Rule_Set.id
+  | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
 
   | Specify_Method of Celem.metID
   | Specify_Problem of Celem.pblID
@@ -315,11 +315,11 @@
   | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
   | rule2tac _ subst (Rule.Thm thm'') = 
     Rewrite_Inst (Selem.subst2subs subst, thm'')
-  | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.rls2str rls)
+  | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
   | rule2tac _ subst (Rule.Rls_ rls) = 
-    Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
+    Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id rls))
   | rule2tac _ _ rule = 
-    error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
+    error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
 
 (* tactics for for internal use, compare "input" for user at the front-end.
   tac_ contains results from check in 'fun applicable_in'.
@@ -437,12 +437,12 @@
   | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
   | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
   | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
-    "," ^ Rule_Set.rls2str rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
+    "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term2str f ^ ",(" ^ UnparseC.term2str f' ^ "," ^ UnparseC.terms2str asm ^ "))"
   | End_Detail' _ => "End_Detail' xxx"
   | Detail_Set' _ => "Detail_Set' xxx"
   | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
 
-  | Derive' rls => "Derive' " ^ Rule_Set.rls2str rls
+  | Derive' rls => "Derive' " ^ Rule_Set.id rls
   | Calculate'  _ => "Calculate' "
   | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    
 
@@ -468,13 +468,13 @@
   | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
   | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
 
-  | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.rls2str rls)
-  | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.rls2str rls)
+  | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
+  | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
 
   | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = 
-    Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
+    Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
   | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) = 
-    Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.rls2str rls)
+    Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
 
   | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
   | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred