1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -36,10 +36,10 @@
     1.4  val thy = @{theory Complex_Main};
     1.5  val ctxt = @{context};
     1.6  val thm = @{thm add.commute};
     1.7 -val t = (term_of o the) (parse thy "((r + u) + t) + s");
     1.8 +val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
     1.9  "----- from old: fun rewrite__";
    1.10  val bdv = [];
    1.11 -val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
    1.12 +val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
    1.13  "----- from old: and rew_sub";
    1.14  val (LHS,RHS) = (dest_equals' o strip_trueprop 
    1.15     	      o Logic.strip_imp_concl) r;
    1.16 @@ -162,11 +162,11 @@
    1.17  "----------- step through 'and rew_sub': ----------------";
    1.18  (*and make asms without Trueprop, beginning with the result:*)
    1.19  val tm = @{term "x*y / y::real"};
    1.20 -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
    1.21 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;
    1.22  (*show_types := false;*)
    1.23  "----- evaluate arguments";
    1.24  val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
    1.25 -    (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
    1.26 +    (thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm);
    1.27  "----- step 1: LHS, RHS of rule";
    1.28       val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.29                         o Logic.strip_imp_concl) r;
    1.30 @@ -315,7 +315,7 @@
    1.31  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
    1.32  (*t' = t''; (*false because of further rewrites in t'*)*)
    1.33  "----- rew_sub  --------------------------------";
    1.34 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
    1.35 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
    1.36  (*t'' = t'''; (*true*)*)
    1.37  "----- rewrite_set_ erls --------------------------------";
    1.38  val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
    1.39 @@ -334,7 +334,7 @@
    1.40  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
    1.41  (*t' = t''; (*false because of further rewrites in t'*)*)
    1.42  writeln "----- rew_sub  --------------------------------";
    1.43 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
    1.44 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
    1.45  (*t'' = t'''; (*true*)*)
    1.46  writeln "----- rewrite_set_ erls --------------------------------";
    1.47  val cond = @{term "(x / x ^^^ 2)"};
    1.48 @@ -502,7 +502,7 @@
    1.49  "----------- 2011 thms with axclasses -------------------";
    1.50  "----------- 2011 thms with axclasses -------------------";
    1.51  val thm = num_str @{thm divide_1};
    1.52 -val prop = prop_of thm;
    1.53 +val prop = Thm.prop_of thm;
    1.54  atomty prop;                                     (*Type 'a*)
    1.55  val t = str2term "(2*x)/1";                      (*Type real*)
    1.56