diff -r fac82f29f143 -r eb7d9cbaa3ef src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Sep 08 17:49:36 2010 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Sep 08 17:55:08 2010 +0200
@@ -13,9 +13,9 @@
   is'_f'_x            :: "real => bool"        ("_ is'_f'_x" 10)
 
   (*descriptions in the related problems*)
-  integrateBy         :: real => una
-  antiDerivative      :: real => una
-  antiDerivativeName  :: (real => real) => una
+  integrateBy         :: "real => una"
+  antiDerivative      :: "real => una"
+  antiDerivativeName  :: "(real => real) => una"
 
   (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
   Integrate           :: "[real * real] => real"
@@ -113,8 +113,8 @@
     ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
     ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
     ]);
-
-
+*}
+ML {*
 (** rulesets **)
 
 (*.rulesets for integration.*)
@@ -143,6 +143,8 @@
 		  Calc ("op +", eval_binop "#add_")(*for n+1*)
 		  ],
 	 scr = EmptyScr};
+*}
+ML {*
 val add_new_c = 
     Seq {id="add_new_c", preconds = [], 
 	 rew_ord = ("termlessI",termlessI), 
@@ -155,7 +157,7 @@
 			      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_false",num_str @{thm not_false})
 			      ],
 		     scr = EmptyScr}, 
 	 srls = Erls, calc = [],
@@ -163,6 +165,8 @@
 		   Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
 		   ],
 	 scr = EmptyScr};
+*}
+ML {*
 
 (*.rulesets for simplifying Integrals.*)
 
@@ -331,6 +335,8 @@
 	     ("norm_Rational_rls_noadd_fractions", 
 	      norm_Rational_rls_noadd_fractions)
 	     ]);
+*}
+ML {*
 
 (** problems **)
 
@@ -338,7 +344,7 @@
  (prep_pbt thy "pbl_fun_integ" [] e_pblID
  (["integrate","function"],
   [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-   ("#Find"  ,["antiDerivative F_"])
+   ("#Find"  ,["antiDerivative F_F"])
   ],
   append_rls "e_rls" e_rls [(*for preds in where_*)], 
   SOME "Integrate (f_f, v_v)", 
@@ -349,43 +355,47 @@
  (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
  (["named","integrate","function"],
   [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-   ("#Find"  ,["antiDerivativeName F_"])
+   ("#Find"  ,["antiDerivativeName F_F"])
   ],
   append_rls "e_rls" e_rls [(*for preds in where_*)], 
   SOME "Integrate (f_f, v_v)", 
   [["diff","integration","named"]]));
  
+*}
+ML {*
 (** methods **)
 
 store_met
     (prep_met thy "met_diffint" [] e_metID
 	      (["diff","integration"],
 	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-		("#Find"  ,["antiDerivative F_"])
+		("#Find"  ,["antiDerivative F_F"])
 		],
 	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 
 		srls = e_rls, 
 		prls=e_rls,
 	     crls = Atools_erls, nrls = e_rls},
 "Script IntegrationScript (f_f::real) (v_v::real) =                " ^
-"  (let t_ = Take (Integral f_ D v_v)                             " ^
-"   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"
+"  (let t_t = Take (Integral f_f D v_v)                             " ^
+"   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"
 ));
-    
+  *}
+ML {*
+
 store_met
     (prep_met thy "met_diffint_named" [] e_metID
 	      (["diff","integration","named"],
 	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
-		("#Find"  ,["antiDerivativeName F_"])
+		("#Find"  ,["antiDerivativeName F_F"])
 		],
 	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 
 		srls = e_rls, 
 		prls=e_rls,
 		crls = Atools_erls, nrls = e_rls},
-"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = " ^
-"  (let t_ = Take (F_ v_v = Integral f_ D v_v)                            " ^
+"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
+"  (let t_t = Take (F_F v_v = Integral f_f D v_v)                            " ^
 "   in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@  " ^
-"       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_)            "
+"       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t)            "
     ));
 *}