1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Sat Apr 17 20:44:57 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Sat Apr 17 21:10:27 2021 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  fun rewrite__ thy i bdv tless rls put_asm thm ct =
     1.5    let
     1.6      val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
     1.7 -		  (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct
     1.8 +		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
     1.9    in if rew then SOME (t', distinct op = asms) else NONE end
    1.10    (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
    1.11  and rew_sub thy i bdv tless rls put_asm lrd r t =