1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  
     1.6  (*
     1.7 -> val t = (term_of o the o (parse thy)) "#2^^^#3";
     1.8 +> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
     1.9  > val eval_fn = the (assoc (!eval_list, "pow"));
    1.10  > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
    1.11  > Syntax.string_of_term (thy2ctxt thy) t';
    1.12 @@ -120,7 +120,7 @@
    1.13  parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
    1.14  (* 31.1.00 
    1.15  val tag__forms = chktyps thy (formals, givens);
    1.16 -map ((atomty) o term_of) tag__forms;       *)
    1.17 +map ((atomty) o Thm.term_of) tag__forms;       *)
    1.18  
    1.19  " --- subproblem 2: linear-equation --- ";
    1.20  val origin = ["x + 4 = (0::real)","x::real"];
    1.21 @@ -135,14 +135,14 @@
    1.22  val givens = map (the o (parse thy)) given;
    1.23  
    1.24  val tag__forms = chktyps thy (formals, givens);
    1.25 -map ((atomty) o term_of) tag__forms;
    1.26 +map ((atomty) o Thm.term_of) tag__forms;
    1.27  
    1.28  
    1.29  
    1.30  " _________________ rewrite_ x+4_________________ ";
    1.31  " _________________ rewrite_ x+4_________________ ";
    1.32  " _________________ rewrite_ x+4_________________ ";
    1.33 -val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.34 +val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.35  val thm = num_str @{thm square_equation_left};
    1.36  val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
    1.37  val rls = Test_simplify;
    1.38 @@ -210,8 +210,8 @@
    1.39  " _________________ rewrite x=4_________________ ";
    1.40  (*
    1.41  rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct;
    1.42 -atomty ((#prop o rep_thm) (!tthm));
    1.43 -atomty (term_of (!tct));
    1.44 +atomty ((#prop o Thm.rep_thm) (!tthm));
    1.45 +atomty (Thm.term_of (!tct));
    1.46  *)
    1.47  val thy' = "Test";
    1.48  val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
    1.49 @@ -385,7 +385,7 @@
    1.50  *)
    1.51  
    1.52  (*
    1.53 -val t = (term_of o the o (parse thy)) "solutions (L::real set)";
    1.54 +val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";
    1.55  atomty t;
    1.56  *)
    1.57  
    1.58 @@ -573,7 +573,7 @@
    1.59  
    1.60  
    1.61  
    1.62 -val ttt = (term_of o the o (parse Test.thy))
    1.63 +val ttt = (Thm.term_of o the o (parse Test.thy))
    1.64  "Let (((While contains_root e_e Do\
    1.65  \Rewrite square_equation_left True @@\
    1.66  \Try (Rewrite_Set Test_simplify False) @@\