1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Sun Apr 25 12:49:37 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Apr 26 14:16:35 2021 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4      val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
     1.5  		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
     1.6    in if rew then SOME (t', distinct op = asms) else NONE end
     1.7 -  (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
     1.8 +  (* one rewrite (possibly conditional, ordered) EXOR exn Pattern.MATCH EXOR go into subterms *)
     1.9  and rew_sub thy i bdv tless rls put_asm lrd r t = 
    1.10    (let
    1.11      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r