1.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Mon Sep 06 14:48:38 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Mon Sep 06 15:09:37 2010 +0200
     1.3 @@ -314,7 +314,7 @@
     1.4  "----------- check probem type -----------------------------------";
     1.5  "----------- check probem type -----------------------------------";
     1.6  "----------- check probem type -----------------------------------";
     1.7 -val model = {Given =["functionTerm f_", "integrateBy v_"],
     1.8 +val model = {Given =["functionTerm f_", "integrateBy v_v"],
     1.9  	     Where =[],
    1.10  	     Find  =["antiDerivative F_"],
    1.11  	     With  =[],
    1.12 @@ -326,7 +326,7 @@
    1.13  case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
    1.14  	 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
    1.15  
    1.16 -val model = {Given =["functionTerm f_", "integrateBy v_"],
    1.17 +val model = {Given =["functionTerm f_", "integrateBy v_v"],
    1.18  	     Where =[],
    1.19  	     Find  =["antiDerivativeName F_"],
    1.20  	     With  =[],
    1.21 @@ -363,14 +363,14 @@
    1.22  "----------- check Scripts ---------------------------------------";
    1.23  val str = 
    1.24  "Script IntegrationScript (f_::real) (v_::real) =               \
    1.25 -\  (let t_ = Take (Integral f_ D v_)                                 \
    1.26 +\  (let t_ = Take (Integral f_ D v_v)                                 \
    1.27  \   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
    1.28  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.29  atomty sc;
    1.30  
    1.31  val str = 
    1.32  "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \
    1.33 -\  (let t_ = Take (F_ v_ = Integral f_ D v_)                         \
    1.34 +\  (let t_ = Take (F_ v_v = Integral f_ D v_v)                         \
    1.35  \   in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
    1.36  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.37  atomty sc;
    1.38 @@ -479,7 +479,7 @@
    1.39  store_met
    1.40      (prep_met Integrate.thy "met_testint" [] e_metID
    1.41  	      (["diff","integration","test"],
    1.42 -	       [("#Given" ,["functionTerm f_", "integrateBy v_"]),
    1.43 +	       [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
    1.44  		("#Find"  ,["antiDerivative F_"])
    1.45  		],
    1.46  	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [],