1.1 --- a/test/Tools/isac/OLDTESTS/script.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/OLDTESTS/script.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4     \                    [BOOL e_2, REAL v_2])\
     1.5     \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
     1.6  
     1.7 -val ags = map (term_of o the o (parse DiffApp.thy)) 
     1.8 +val ags = map (Thm.term_of o the o (parse DiffApp.thy)) 
     1.9    ["A::real", "alpha::real", 
    1.10     "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
    1.11  val ll = [](*:loc_*);
    1.12 @@ -156,7 +156,7 @@
    1.13  (*#####################################################--------11.5.02
    1.14  "################ Solve_root_equation #################";
    1.15  (*#####################################################*)
    1.16 -val sc = (term_of o the o (parse Test.thy))
    1.17 +val sc = (Thm.term_of o the o (parse Test.thy))
    1.18    "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
    1.19     \ (let e_e = Rewrite square_equation_left True eq_;     \
    1.20     \      e_e = Rewrite_Set Test_simplify False e_;          \
    1.21 @@ -172,7 +172,7 @@
    1.22     \      e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
    1.23     \      e_e = Rewrite_Set Test_simplify False e_e       \
    1.24     \ in [e_::bool])";
    1.25 -val ags = map (term_of o the o (parse Test.thy)) 
    1.26 +val ags = map (Thm.term_of o the o (parse Test.thy)) 
    1.27    ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
    1.28  val fmz = 
    1.29    ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
    1.30 @@ -248,7 +248,7 @@
    1.31  "  --- test100:  nxt_tac order------------------------------------ ";
    1.32  
    1.33  val scr as (Prog sc) = Prog (((inst_abs Test.thy) 
    1.34 -				  o term_of o the o (parse thy))
    1.35 +				  o Thm.term_of o the o (parse thy))
    1.36   "Script Testeq (e_e::bool) =                                        \
    1.37     \(While (contains_root e_e) Do                                     \
    1.38     \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \
    1.39 @@ -266,10 +266,10 @@
    1.40  val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
    1.41  val (p,_,_,_,_,pt) = me nxt p c pt;
    1.42  val p = ([1],Res):pos';
    1.43 -val eq_ = (term_of o the o (parse thy))"e_::bool";
    1.44 +val eq_ = (Thm.term_of o the o (parse thy))"e_::bool";
    1.45  
    1.46  val ct =   "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
    1.47 -val ve0_= (term_of o the o (parse thy)) ct;
    1.48 +val ve0_= (Thm.term_of o the o (parse thy)) ct;
    1.49  val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
    1.50  	       e_term,e_term,Safe)),
    1.51  	  ([],(User', [],                [],        e_term, e_term,Sundef))]:ets;
    1.52 @@ -282,14 +282,14 @@
    1.53  
    1.54  
    1.55  val scr as (Prog sc) = 
    1.56 -    Prog (((inst_abs Test.thy)  o term_of o the o (parse thy)) 
    1.57 +    Prog (((inst_abs Test.thy)  o Thm.term_of o the o (parse thy)) 
    1.58   "Script Testterm (g_::real) = (Calculate cancel g_)");
    1.59  (*
    1.60  val scr as (Prog sc) = 
    1.61 -    Prog (((inst_abs Test.thy)  o term_of o the o (parse thy)) 
    1.62 +    Prog (((inst_abs Test.thy)  o Thm.term_of o the o (parse thy)) 
    1.63   "Script Testterm (g_::real) = (Calculate power g_)");
    1.64  val scr as (Prog sc) = 
    1.65 -    Prog (((inst_abs Test.thy)  o term_of o the o (parse thy)) 
    1.66 +    Prog (((inst_abs Test.thy)  o Thm.term_of o the o (parse thy)) 
    1.67   "Script Testterm (g_::real) = (Calculate pow g_)");
    1.68  ..............................................................*)
    1.69  writeln