1.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Wed Oct 06 14:35:43 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Wed Oct 06 14:52:12 2010 +0200
     1.3 @@ -341,10 +341,9 @@
     1.4  case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
     1.5  	 | _ => error "integrate.sml: Integrate.antiDerivative ???";
     1.6  
     1.7 -(*=== inhibit exn ?=============================================================
     1.8  val model = {Given =["functionTerm f_f", "integrateBy v_v"],
     1.9  	     Where =[],
    1.10 -	     Find  =["antiDerivativeName F_"],
    1.11 +	     Find  =["antiDerivativeName F_F"],
    1.12  	     With  =[],
    1.13  	     Relate=[]}:string ppc;
    1.14  val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
    1.15 @@ -357,7 +356,7 @@
    1.16  "----- compare 'Find's from problem, script, formalization -------";
    1.17  val {ppc,...} = get_pbt ["named","integrate","function"];
    1.18  val ("#Find", (Const ("Integrate.antiDerivativeName", _),
    1.19 -	       F1_ as Free ("F_", F1_type))) = last_elem ppc;
    1.20 +	       F1_ as Free ("F_F", F1_type))) = last_elem ppc;
    1.21  val {scr = Script sc,... } = get_met ["diff","integration","named"];
    1.22  val [_,_, F2_] = formal_args sc;
    1.23  if F1_ = F2_ then () else error "integrate.sml: unequal find's";
    1.24 @@ -379,15 +378,15 @@
    1.25  "----------- check Scripts ------------------------------";
    1.26  val str = 
    1.27  "Script IntegrationScript (f_f::real) (v_v::real) =               \
    1.28 -\  (let t_ = Take (Integral f_ D v_v)                                 \
    1.29 -\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";
    1.30 +\  (let t_t = Take (Integral f_f D v_v)                                 \
    1.31 +\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";
    1.32  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.33  atomty sc;
    1.34  
    1.35  val str = 
    1.36 -"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \
    1.37 -\  (let t_ = Take (F_ v_v = Integral f_ D v_v)                         \
    1.38 -\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";
    1.39 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
    1.40 +\  (let t_t = Take (F_F v_v = Integral f_f D v_v)                         \
    1.41 +\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";
    1.42  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.43  atomty sc;
    1.44  show_mets();
    1.45 @@ -418,6 +417,7 @@
    1.46  else error "integrate.sml: method [diff,integration]";
    1.47  
    1.48  
    1.49 +(*=== inhibit exn ?=============================================================
    1.50  "----------- me method [diff,integration,named] ---------";
    1.51  "----------- me method [diff,integration,named] ---------";
    1.52  "----------- me method [diff,integration,named] ---------";
    1.53 @@ -496,7 +496,7 @@
    1.54      (prep_met thy "met_testint" [] e_metID
    1.55  	      (["diff","integration","test"],
    1.56  	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.57 -		("#Find"  ,["antiDerivative F_"])
    1.58 +		("#Find"  ,["antiDerivative F_F"])
    1.59  		],
    1.60  	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 
    1.61  		srls = e_rls,