
diff -r 0042fe0bc764 -r 82428ca0d23e src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Apr 13 13:27:55 2020 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Apr 13 15:31:23 2020 +0200
@@ -119,17 +119,17 @@
 		     srls = Rule_Set.Empty, calc = [], errpatts = [],
 		     rules = [(*for rewriting conditions in Thm's*)
 			      Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
-			      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
+			      Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
 			      Rule.Thm ("not_false",@{thm not_false})
 			      ],
 		     scr = Rule.EmptyScr}, 
 	 srls = Rule_Set.Empty, calc = [], errpatts = [],
 	 rules = [
-		  Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}),
-		  Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}),
-		  Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}),
-		  Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
-		  Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
+		  Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}),
+		  Rule.Thm ("integral_var", ThmC.numerals_to_Free @{thm integral_var}),
+		  Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
+		  Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
+		  Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
 		  Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
 		  ],
 	 scr = Rule.EmptyScr};
@@ -146,12 +146,12 @@
 		     rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
 			      Rule.Num_Calc ("Integrate.is'_f'_x", 
 				    eval_is_f_x "is_f_x_"),
-			      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
-			      Rule.Thm ("not_false", TermC.num_str @{thm not_false})
+			      Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
+			      Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
 			      ],
 		     scr = Rule.EmptyScr}, 
 	 srls = Rule_Set.Empty, calc = [], errpatts = [],
-	 rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
+	 rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
 		   Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
 		   ],
 	 scr = Rule.EmptyScr};
@@ -174,25 +174,25 @@
 				  [Rule.Num_Calc ("Poly.is'_polyexp", 
 					 eval_is_polyexp "")],
 				  srls = Rule_Set.Empty, calc = [], errpatts = [],
-				  rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
+				  rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
 	       (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
-	       Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
+	       Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
 	       (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
-	       Rule.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
+	       Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
 	       (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
 
 	       Rule.Thm ("real_divide_divide1_mg",
-                     TermC.num_str @{thm real_divide_divide1_mg}),
+                     ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
 	       (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
 	       Rule.Thm ("divide_divide_eq_right", 
-                     TermC.num_str @{thm divide_divide_eq_right}),
+                     ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
 	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
 	       Rule.Thm ("divide_divide_eq_left",
-                     TermC.num_str @{thm divide_divide_eq_left}),
+                     ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
 	       Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
 	      
-	       Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
+	       Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
 	       ],
       scr = Rule.EmptyScr
@@ -228,15 +228,15 @@
 val separate_bdv2 =
     Rule_Set.append_rules "separate_bdv2"
 	       collect_bdv
-	       [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
+	       [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
 		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
-		Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
-		Rule.Thm ("separate_1_bdv",  TermC.num_str @{thm separate_1_bdv}),
+		Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
+		Rule.Thm ("separate_1_bdv",  ThmC.numerals_to_Free @{thm separate_1_bdv}),
 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
-		Rule.Thm ("separate_1_bdv_n",  TermC.num_str @{thm separate_1_bdv_n})(*,
+		Rule.Thm ("separate_1_bdv_n",  ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
 			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
 			  *****Rule.Thm ("add_divide_distrib", 
-			  ***** TermC.num_str @{thm add_divide_distrib})
+			  ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
 			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
 		];
 val simplify_Integral = 
@@ -244,9 +244,9 @@
        rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
       erls = Atools_erls, srls = Rule_Set.Empty,
       calc = [],  errpatts = [],
-      rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
+      rules = [Rule.Thm ("distrib_right", ThmC.numerals_to_Free @{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}),
+	       Rule.Thm ("add_divide_distrib", ThmC.numerals_to_Free @{thm add_divide_distrib}),
  	       (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
 	       (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
 	       Rule.Rls_ norm_Rational_noadd_fractions,
@@ -275,21 +275,21 @@
 * 	       Rule.Rls_ simplify_power,
 * 	       Rule.Rls_ collect_numerals,
 * 	       Rule.Rls_ reduce_012,
-* 	       Rule.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
+* 	       Rule.Thm ("realpow_oneI", ThmC.numerals_to_Free @{thm realpow_oneI}),
 * 	       Rule.Rls_ discard_parentheses,
 * 	       Rule.Rls_ collect_bdv,
 * 	       (*below inserted from 'make_ratpoly_in'*)
 * 	       Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
 * 			 collect_bdv
-* 			 [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
+* 			 [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
 * 			  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
-* 			  Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
-* 			  Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
+* 			  Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
+* 			  Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
 * 			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
-* 			  Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
+* 			  Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
 * 			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
 * 			  Rule.Thm ("add_divide_distrib", 
-* 				  TermC.num_str @{thm add_divide_distrib})
+* 				  ThmC.numerals_to_Free @{thm add_divide_distrib})
 * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
 * 			  ]),
 * 	       Rule.Num_Calc ("Rings.divide_class.divide"  , eval_cancel "#divide_e")




