diff -r 2cbb98890190 -r 3e241a6938ce src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Mar 15 15:48:52 2018 +0100
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Fri Mar 23 10:14:39 2018 +0100
@@ -294,7 +294,7 @@
 ML {*
 val isolate_bdvs = 
     Celem.Rls {id="isolate_bdvs", preconds = [], 
-	 rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), 
+	 rew_ord = ("e_rew_ord", Celem.e_rew_ord), 
 	 erls = Celem.append_rls "erls_isolate_bdvs" Celem.e_rls 
 			   [(Celem.Calc ("EqSystem.occur'_exactly'_in", 
 				   eval_occur_exactly_in 
@@ -310,7 +310,7 @@
 ML {*
 val isolate_bdvs_4x4 = 
     Celem.Rls {id="isolate_bdvs_4x4", preconds = [], 
-	 rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), 
+	 rew_ord = ("e_rew_ord", Celem.e_rew_ord), 
 	 erls = Celem.append_rls 
 		    "erls_isolate_bdvs_4x4" Celem.e_rls 
 		    [Celem.Calc ("EqSystem.occur'_exactly'_in", 
@@ -345,9 +345,9 @@
 
 val prls_triangular = 
     Celem.Rls {id="prls_triangular", preconds = [], 
-	 rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), 
+	 rew_ord = ("e_rew_ord", Celem.e_rew_ord), 
 	 erls = Celem.Rls {id="erls_prls_triangular", preconds = [], 
-		     rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), 
+		     rew_ord = ("e_rew_ord", Celem.e_rew_ord), 
 		     erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
@@ -374,9 +374,9 @@
  more similarity to prls_triangular desirable*)
 val prls_triangular4 = 
     Celem.Rls {id="prls_triangular4", preconds = [], 
-	 rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), 
+	 rew_ord = ("e_rew_ord", Celem.e_rew_ord), 
 	 erls = Celem.Rls {id="erls_prls_triangular4", preconds = [], 
-		     rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), 
+		     rew_ord = ("e_rew_ord", Celem.e_rew_ord), 
 		     erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
@@ -416,13 +416,13 @@
       (["system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"](*''' is copy-named*))],
-        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
+        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
     (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
       (["LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           (*TODO.WN050929 check linearity*)
           ("#Find"  ,["solution ss'''"])],
-        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
+        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
     (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
       (["2x2", "LINEAR", "system"],
       (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
@@ -447,7 +447,7 @@
       (["normalise", "2x2", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"])],
-      Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], 
+      Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], 
       SOME "solveSystem e_s v_s", 
       [["EqSystem","normalise","2x2"]])),
     (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
@@ -492,7 +492,7 @@
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           (*LENGTH is checked 1 level above*)
           ("#Find"  ,["solution ss'''"])],
-        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], 
+        Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], 
         SOME "solveSystem e_s v_s", 
         [["EqSystem","normalise","4x4"]]))] *}