1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Sat Apr 17 20:44:57 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Sat Apr 17 21:10:27 2021 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
     1.5  "----- from old: fun rewrite__";
     1.6  val bdv = [];
     1.7 -val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
     1.8 +val r = inst_bdv bdv (norm (Thm.prop_of thm));
     1.9  "----- from old: and rew_sub";
    1.10  val (LHS,RHS) = (dest_equals o strip_trueprop 
    1.11     	      o Logic.strip_imp_concl) r;
    1.12 @@ -591,10 +591,10 @@
    1.13  
    1.14      val (t', asms, _ (*lrd*), rew) =
    1.15             rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
    1.16 -		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct;
    1.17 +		  (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
    1.18  "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
    1.19    = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
    1.20 -		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm), ct);
    1.21 +		  (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
    1.22      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
    1.23      val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
    1.24  ;
    1.25 @@ -688,7 +688,7 @@
    1.26  "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
    1.27    (thy, 1, [], rew_ord, erls, bool, thm, term);
    1.28  "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
    1.29 -  (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
    1.30 +  (thy, i, bdv, tless, rls, put_asm, [], inst_bdv bdv (norm (Thm.prop_of thm)), ct)
    1.31       val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
    1.32       val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
    1.33       val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))