
diff -r d82a32869f27 -r f3cac3053e7b src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Apr 01 19:20:05 2020 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sat Apr 04 12:11:32 2020 +0200
@@ -170,10 +170,10 @@
 
 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
 val order_add_mult_System = 
-  Rule.Rls{id = "order_add_mult_System", preconds = [], 
+  Rule_Set.Rls{id = "order_add_mult_System", preconds = [], 
       rew_ord = ("ord_simplify_System",
 		 ord_simplify_System false @{theory "Integrate"}),
-      erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
+      erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [],
       rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
 	       (* z * w = w * z *)
 	       Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
@@ -194,9 +194,9 @@
   #1 using 'ord_simplify_System' in 'order_add_mult_System'
   #2 NOT using common_nominator_p                          .*)
 val norm_System_noadd_fractions = 
-  Rule.Rls {id = "norm_System_noadd_fractions", preconds = [], 
+  Rule_Set.Rls {id = "norm_System_noadd_fractions", preconds = [], 
        rew_ord = ("dummy_ord",Rule.dummy_ord), 
-       erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
+       erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
        rules = [(*sequence given by operator precedence*)
 		Rule.Rls_ discard_minus,
 		Rule.Rls_ powers,
@@ -215,9 +215,9 @@
 (*.adapted from 'norm_Rational' by
   *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
 val norm_System = 
-  Rule.Rls {id = "norm_System", preconds = [], 
+  Rule_Set.Rls {id = "norm_System", preconds = [], 
        rew_ord = ("dummy_ord",Rule.dummy_ord), 
-       erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
+       erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
        rules = [(*sequence given by operator precedence*)
 		Rule.Rls_ discard_minus,
 		Rule.Rls_ powers,
@@ -243,9 +243,9 @@
    *3* discard_parentheses only for (.*(.*.))
    analoguous to simplify_Integral                                       .*)
 val simplify_System_parenthesized = 
-  Rule.Seq {id = "simplify_System_parenthesized", preconds = []:term list, 
+  Rule_Set.Seq {id = "simplify_System_parenthesized", preconds = []:term list, 
        rew_ord = ("dummy_ord", Rule.dummy_ord),
-      erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
+      erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
       rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
  	       (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
 	       Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
@@ -268,9 +268,9 @@
    *1* ord_simplify_System instead of termlessI           .*)
 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
 val simplify_System = 
-  Rule.Seq {id = "simplify_System", preconds = []:term list, 
+  Rule_Set.Seq {id = "simplify_System", preconds = []:term list, 
        rew_ord = ("dummy_ord", Rule.dummy_ord),
-      erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
+      erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
       rules = [Rule.Rls_ norm_Rational,
 	       Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
 	       Rule.Rls_ discard_parentheses,
@@ -281,21 +281,21 @@
       scr = Rule.EmptyScr};      
 (*
 val simplify_System = 
-    Rule.append_rls "simplify_System" simplify_System_parenthesized
+    Rule_Set.append_rls "simplify_System" simplify_System_parenthesized
 	       [Rule.Thm ("sym_add_assoc",
                       TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
 *)
 \<close>
 ML \<open>
 val isolate_bdvs = 
-    Rule.Rls {id="isolate_bdvs", preconds = [], 
+    Rule_Set.Rls {id="isolate_bdvs", preconds = [], 
 	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
-	 erls = Rule.append_rls "erls_isolate_bdvs" Rule.e_rls 
+	 erls = Rule_Set.append_rls "erls_isolate_bdvs" Rule_Set.e_rls 
 			   [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in", 
 				   eval_occur_exactly_in 
 				       "#eval_occur_exactly_in_"))
 			    ], 
-			   srls = Rule.Erls, calc = [], errpatts = [],
+			   srls = Rule_Set.Erls, calc = [], errpatts = [],
 	      rules = 
              [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
 	      Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
@@ -304,10 +304,10 @@
 \<close>
 ML \<open>
 val isolate_bdvs_4x4 = 
-    Rule.Rls {id="isolate_bdvs_4x4", preconds = [], 
+    Rule_Set.Rls {id="isolate_bdvs_4x4", preconds = [], 
 	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
-	 erls = Rule.append_rls 
-		    "erls_isolate_bdvs_4x4" Rule.e_rls 
+	 erls = Rule_Set.append_rls 
+		    "erls_isolate_bdvs_4x4" Rule_Set.e_rls 
 		    [Rule.Num_Calc ("EqSystem.occur'_exactly'_in", 
 			   eval_occur_exactly_in "#eval_occur_exactly_in_"),
 		     Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
@@ -315,7 +315,7 @@
          Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
 		     Rule.Thm ("not_false",TermC.num_str @{thm not_false})
 			    ], 
-	 srls = Rule.Erls, calc = [], errpatts = [],
+	 srls = Rule_Set.Erls, calc = [], errpatts = [],
 	 rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
 		  Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
 		  Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
@@ -329,20 +329,20 @@
 (*.order the equations in a system such, that a triangular system (if any)
    appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
 val order_system = 
-    Rule.Rls {id="order_system", preconds = [], 
+    Rule_Set.Rls {id="order_system", preconds = [], 
 	 rew_ord = ("ord_simplify_System", 
 		    ord_simplify_System false thy), 
-	 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
+	 erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
 	 rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
 		  ],
 	 scr = Rule.EmptyScr};
 
 val prls_triangular = 
-    Rule.Rls {id="prls_triangular", preconds = [], 
+    Rule_Set.Rls {id="prls_triangular", preconds = [], 
 	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
-	 erls = Rule.Rls {id="erls_prls_triangular", preconds = [], 
+	 erls = Rule_Set.Rls {id="erls_prls_triangular", preconds = [], 
 		     rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
-		     erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
+		     erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
 			      Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
@@ -350,7 +350,7 @@
 					    '+' into precondition !*)
 			      ],
 		     scr = Rule.EmptyScr}, 
-	 srls = Rule.Erls, calc = [], errpatts = [],
+	 srls = Rule_Set.Erls, calc = [], errpatts = [],
 	 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
 		  Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
 		  Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
@@ -367,11 +367,11 @@
 (*WN060914 quickly created for 4x4; 
  more similarity to prls_triangular desirable*)
 val prls_triangular4 = 
-    Rule.Rls {id="prls_triangular4", preconds = [], 
+    Rule_Set.Rls {id="prls_triangular4", preconds = [], 
 	 rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
-	 erls = Rule.Rls {id="erls_prls_triangular4", preconds = [], 
+	 erls = Rule_Set.Rls {id="erls_prls_triangular4", preconds = [], 
 		     rew_ord = ("e_rew_ord", Rule.e_rew_ord), 
-		     erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
+		     erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
 			      Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
@@ -379,7 +379,7 @@
 					    '+' into precondition !*)
 			      ],
 		     scr = Rule.EmptyScr}, 
-	 srls = Rule.Erls, calc = [], errpatts = [],
+	 srls = Rule_Set.Erls, calc = [], errpatts = [],
 	 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
 		  Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
 		  Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
@@ -410,20 +410,20 @@
       (["system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"](*''' is copy-named*))],
-        Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
+        Rule_Set.append_rls "e_rls" Rule_Set.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'''"])],
-        Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
+        Rule_Set.append_rls "e_rls" Rule_Set.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"],
       (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Where"  ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
           ("#Find"  ,["solution ss'''"])],
-        Rule.append_rls "prls_2x2_linear_system" Rule.e_rls 
+        Rule_Set.append_rls "prls_2x2_linear_system" Rule_Set.e_rls 
 			    [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
 			      Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
 			      Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
@@ -441,7 +441,7 @@
       (["normalise", "2x2", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"])],
-      Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], 
+      Rule_Set.append_rls "e_rls" Rule_Set.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
@@ -450,7 +450,7 @@
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Where"  ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
           ("#Find"  ,["solution ss'''"])],
-        Rule.append_rls "prls_3x3_linear_system" Rule.e_rls 
+        Rule_Set.append_rls "prls_3x3_linear_system" Rule_Set.e_rls 
 			    [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
 			      Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
 			      Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
@@ -462,7 +462,7 @@
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Where"  ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
           ("#Find"  ,["solution ss'''"])],
-        Rule.append_rls "prls_4x4_linear_system" Rule.e_rls 
+        Rule_Set.append_rls "prls_4x4_linear_system" Rule_Set.e_rls 
 			    [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
 			      Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
 			      Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
@@ -477,7 +477,7 @@
               "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
               "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
           ("#Find"  ,["solution ss'''"])],
-      Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
+      Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
 	      [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], 
       SOME "solveSystem e_s v_s", 
       [["EqSystem","top_down_substitution","4x4"]])),
@@ -486,22 +486,22 @@
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           (*LENGTH is checked 1 level above*)
           ("#Find"  ,["solution ss'''"])],
-        Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], 
+        Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], 
         SOME "solveSystem e_s v_s", 
         [["EqSystem","normalise","4x4"]]))]\<close>
 
 ML \<open>
 (*this is for NTH only*)
-val srls = Rule.Rls {id="srls_normalise_4x4", 
+val srls = Rule_Set.Rls {id="srls_normalise_4x4", 
 		preconds = [], 
 		rew_ord = ("termlessI",termlessI), 
-		erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
+		erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
 				  [(*for asm in NTH_CONS ...*)
 				   Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
 				   (*2nd NTH_CONS pushes n+-1 into asms*)
 				   Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
 				   ], 
-		srls = Rule.Erls, calc = [], errpatts = [],
+		srls = Rule_Set.Erls, calc = [], errpatts = [],
 		rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
 			 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
 			 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
@@ -512,13 +512,13 @@
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
 	    (["EqSystem"], [],
-	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
-          errpats = [], nrls = Rule.Erls},
+	      {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
+          errpats = [], nrls = Rule_Set.Erls},
 	      @{thm refl}),
     Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
       (["EqSystem","top_down_substitution"], [],
-        {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
-          errpats = [], nrls = Rule.Erls},
+        {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
+          errpats = [], nrls = Rule_Set.Erls},
        @{thm refl})]
 \<close>
 
@@ -549,19 +549,19 @@
             ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
               "    v_s  from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
           ("#Find"  ,["solution ss'''"])],
-	      {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [], 
-	        srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls
+	      {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [], 
+	        srls = Rule_Set.append_rls "srls_top_down_2x2" Rule_Set.e_rls
 				      [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
 				        Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
 				        Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], 
-	        prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
+	        prls = prls_triangular, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
 	      @{thm solve_system.simps})]
 \<close>
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
 	    (["EqSystem", "normalise"], [],
-	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
-          errpats = [], nrls = Rule.Erls},
+	      {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
+          errpats = [], nrls = Rule_Set.Erls},
 	      @{thm refl})]
 \<close>
 
@@ -584,12 +584,12 @@
 	    (["EqSystem","normalise","2x2"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 		      ("#Find"  ,["solution ss'''"])],
-	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], 
-	        srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls
+	      {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], 
+	        srls = Rule_Set.append_rls "srls_normalise_2x2" Rule_Set.e_rls
 				      [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
 				        Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
 				        Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], 
-		      prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
+		      prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
 		    @{thm solve_system2.simps})]
 \<close>
 
@@ -616,12 +616,12 @@
 	      (["EqSystem","normalise","4x4"],
 	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	         ("#Find"  ,["solution ss'''"])],
-	       {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], 
-	         srls = Rule.append_rls "srls_normalise_4x4" srls
+	       {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], 
+	         srls = Rule_Set.append_rls "srls_normalise_4x4" srls
 	             [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
 	               Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
 	               Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], 
-		       prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
+		       prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
 		     (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
 		     @{thm solve_system3.simps})]
 \<close>
@@ -653,11 +653,11 @@
               "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
               "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
 	        ("#Find", ["solution ss'''"])],
-	    {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [], 
-	      srls = Rule.append_rls "srls_top_down_4x4" srls [], 
-	      prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
+	    {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [], 
+	      srls = Rule_Set.append_rls "srls_top_down_4x4" srls [], 
+	      prls = Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
 			      [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], 
-	      crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
+	      crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
 	    (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
 	    @{thm solve_system4.simps})]
 \<close>




