diff -r 89b3eaa34de6 -r 30cd47104ad7 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Aug 29 13:52:47 2019 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Sep 03 12:40:27 2019 +0200
@@ -27,14 +27,14 @@
 
 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
   Rule.append_rls "LinEq_prls" Rule.e_rls 
-	     [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
-	      Rule.Calc ("Tools.matches", Tools.eval_matches ""),
-	      Rule.Calc ("Tools.lhs"    , Tools.eval_lhs ""),
-	      Rule.Calc ("Tools.rhs"    , Tools.eval_rhs ""),
-	      Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
- 	      Rule.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
-	      Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),    
-	      Rule.Calc ("Atools.ident",eval_ident "#ident_"),
+	     [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
+	      Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
+	      Rule.Calc ("Prog_Expr.lhs"    , Prog_Expr.eval_lhs ""),
+	      Rule.Calc ("Prog_Expr.rhs"    , Prog_Expr.eval_rhs ""),
+	      Rule.Calc ("Poly.has'_degree'_in", eval_has_degree_in ""),
+ 	      Rule.Calc ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
+	      Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
+	      Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
 	      Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
 	      Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
 	      Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
@@ -48,8 +48,8 @@
    [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
-     Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
+     Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
+     Rule.Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"),
      *)
     ];
 
@@ -59,8 +59,8 @@
    [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
     (*		
      Don't use
-     Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
-     Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
+     Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
+     Rule.Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"),
      *)
     ];
 \<close>
@@ -76,14 +76,14 @@
        calc = [], errpatts = [],
        rules = [
 		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
-		Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
-		Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
-		Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
+		Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
+		Rule.Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
+		Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
 		(*  Dont use  
-		 Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),		
-		 Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
+		 Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),		
+		 Rule.Calc ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
 		 *)
-		Rule.Calc ("Atools.pow" ,eval_binop "#power_")
+		Rule.Calc ("Prog_Expr.pow" , (**)eval_binop "#power_")
 		],
        scr = Rule.EmptyScr});
 \<close>