
diff -r 47877d6fa35a -r 627d25067f2f src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Sun Feb 25 16:31:17 2018 +0100
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Mar 02 14:19:59 2018 +0100
@@ -58,14 +58,14 @@
     let fun selc var = 
 	    case (Symbol.explode o id_of) var of
 		"c"::[] => true
-	      |	"c"::"_"::is => (case (int_of_str o implode) is of
+	      |	"c"::"_"::is => (case (TermC.int_of_str o implode) is of
 				     SOME _ => true
 				   | NONE => false)
               | _ => false;
 	fun get_coeff c = case (Symbol.explode o id_of) c of
-	      		      "c"::"_"::is => (the o int_of_str o implode) is
+	      		      "c"::"_"::is => (the o TermC.int_of_str o implode) is
 			    | _ => 0;
-        val cs = filter selc (vars term);
+        val cs = filter selc (TermC.vars term);
     in 
 	case cs of
 	    [] => c
@@ -90,10 +90,10 @@
 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
     let val p' = case p of
 		     Const ("HOL.eq", T) $ lh $ rh => 
-		     Const ("HOL.eq", T) $ lh $ mk_add rh (new_c rh)
-		   | p => mk_add p (new_c p)
+		     Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
+		   | p => TermC.mk_add p (new_c p)
     in SOME ((term2str p) ^ " = " ^ term2str p',
-	  Trueprop $ (mk_equality (p, p')))
+	  TermC.Trueprop $ (TermC.mk_equality (p, p')))
     end
   | eval_add_new_c _ _ _ _ = NONE;
 
@@ -101,11 +101,11 @@
 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
 					   $ arg)) _ =
-    if is_f_x arg
+    if TermC.is_f_x arg
     then SOME ((term2str p) ^ " = True",
-	       Trueprop $ (mk_equality (p, @{term True})))
+	       TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
     else SOME ((term2str p) ^ " = False",
-	       Trueprop $ (mk_equality (p, @{term False})))
+	       TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
   | eval_is_f_x _ _ _ _ = NONE;
 *}
 setup {* KEStore_Elems.add_calcs
@@ -126,17 +126,17 @@
 		     rules = [(*for rewriting conditions in Thm's*)
 			      Calc ("Atools.occurs'_in", 
 				    eval_occurs_in "#occurs_in_"),
-			      Thm ("not_true",num_str @{thm not_true}),
+			      Thm ("not_true", @{thm not_true}),
 			      Thm ("not_false",@{thm not_false})
 			      ],
 		     scr = EmptyScr}, 
 	 srls = Erls, calc = [], errpatts = [],
 	 rules = [
-		  Thm ("integral_const",num_str @{thm integral_const}),
-		  Thm ("integral_var",num_str @{thm integral_var}),
-		  Thm ("integral_add",num_str @{thm integral_add}),
-		  Thm ("integral_mult",num_str @{thm integral_mult}),
-		  Thm ("integral_pow",num_str @{thm integral_pow}),
+		  Thm ("integral_const", @{thm integral_const}),
+		  Thm ("integral_var", @{thm integral_var}),
+		  Thm ("integral_add", @{thm integral_add}),
+		  Thm ("integral_mult", @{thm integral_mult}),
+		  Thm ("integral_pow", @{thm integral_pow}),
 		  Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
 		  ],
 	 scr = EmptyScr};
@@ -153,12 +153,12 @@
 		     rules = [Calc ("Tools.matches", eval_matches""),
 			      Calc ("Integrate.is'_f'_x", 
 				    eval_is_f_x "is_f_x_"),
-			      Thm ("not_true",num_str @{thm not_true}),
-			      Thm ("not_false",num_str @{thm not_false})
+			      Thm ("not_true", @{thm not_true}),
+			      Thm ("not_false", @{thm not_false})
 			      ],
 		     scr = EmptyScr}, 
 	 srls = Erls, calc = [], errpatts = [],
-	 rules = [ (*Thm ("call_for_new_c", num_str @{thm call_for_new_c}),*)
+	 rules = [ (*Thm ("call_for_new_c",  @{thm call_for_new_c}),*)
 		   Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
 		   ],
 	 scr = EmptyScr};
@@ -181,34 +181,34 @@
 				  [Calc ("Poly.is'_polyexp", 
 					 eval_is_polyexp "")],
 				  srls = Erls, calc = [], errpatts = [],
-				  rules = [Thm ("rat_mult",num_str @{thm rat_mult}),
+				  rules = [Thm ("rat_mult", @{thm rat_mult}),
 	       (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
-	       Thm ("rat_mult_poly_l",num_str @{thm rat_mult_poly_l}),
+	       Thm ("rat_mult_poly_l", @{thm rat_mult_poly_l}),
 	       (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
-	       Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}),
+	       Thm ("rat_mult_poly_r", @{thm rat_mult_poly_r}),
 	       (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
 
 	       Thm ("real_divide_divide1_mg",
-                     num_str @{thm real_divide_divide1_mg}),
+                      @{thm real_divide_divide1_mg}),
 	       (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
 	       Thm ("divide_divide_eq_right", 
-                     num_str @{thm divide_divide_eq_right}),
+                      @{thm divide_divide_eq_right}),
 	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
 	       Thm ("divide_divide_eq_left",
-                     num_str @{thm divide_divide_eq_left}),
+                      @{thm divide_divide_eq_left}),
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
 	       Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e"),
 	      
-	       Thm ("rat_power", num_str @{thm rat_power})
+	       Thm ("rat_power",  @{thm rat_power})
 		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
 	       ],
-      scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
+      scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
       }),
 		Rls_ make_rat_poly_with_parentheses,
 		Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
 		Rls_ rat_reduce_1
 		],
-       scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
+       scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
        }:rls;
 
 (*.for simplify_Integral adapted from 'norm_Rational'.*)
@@ -223,7 +223,7 @@
 		Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#)   *)
 		Rls_ discard_parentheses1 (* mult only                       *)
 		],
-       scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
+       scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
        }:rls;
 
 (*.simplify terms before and after Integration such that  
@@ -235,15 +235,15 @@
 val separate_bdv2 =
     append_rls "separate_bdv2"
 	       collect_bdv
-	       [Thm ("separate_bdv", num_str @{thm separate_bdv}),
+	       [Thm ("separate_bdv",  @{thm separate_bdv}),
 		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
-		Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
-		Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
+		Thm ("separate_bdv_n",  @{thm separate_bdv_n}),
+		Thm ("separate_1_bdv",  @{thm separate_1_bdv}),
 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
-		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
+		Thm ("separate_1_bdv_n",  @{thm separate_1_bdv_n})(*,
 			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
 			  *****Thm ("add_divide_distrib", 
-			  *****num_str @{thm add_divide_distrib})
+			  ***** @{thm add_divide_distrib})
 			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
 		];
 val simplify_Integral = 
@@ -251,9 +251,9 @@
        rew_ord = ("dummy_ord", dummy_ord),
       erls = Atools_erls, srls = Erls,
       calc = [],  errpatts = [],
-      rules = [Thm ("distrib_right",num_str @{thm distrib_right}),
+      rules = [Thm ("distrib_right", @{thm distrib_right}),
  	       (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
-	       Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
+	       Thm ("add_divide_distrib", @{thm add_divide_distrib}),
  	       (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
 	       (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
 	       Rls_ norm_Rational_noadd_fractions,
@@ -282,21 +282,21 @@
 * 	       Rls_ simplify_power,
 * 	       Rls_ collect_numerals,
 * 	       Rls_ reduce_012,
-* 	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
+* 	       Thm ("realpow_oneI", @{thm realpow_oneI}),
 * 	       Rls_ discard_parentheses,
 * 	       Rls_ collect_bdv,
 * 	       (*below inserted from 'make_ratpoly_in'*)
 * 	       Rls_ (append_rls "separate_bdv"
 * 			 collect_bdv
-* 			 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
+* 			 [Thm ("separate_bdv",  @{thm separate_bdv}),
 * 			  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
-* 			  Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
-* 			  Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
+* 			  Thm ("separate_bdv_n",  @{thm separate_bdv_n}),
+* 			  Thm ("separate_1_bdv",  @{thm separate_1_bdv}),
 * 			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
-* 			  Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
+* 			  Thm ("separate_1_bdv_n",  @{thm separate_1_bdv_n})(*,
 * 			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
 * 			  Thm ("add_divide_distrib", 
-* 				 num_str @{thm add_divide_distrib})
+* 				  @{thm add_divide_distrib})
 * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
 * 			  ]),
 * 	       Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e")




