1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 27 18:09:22 2021 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Tue Apr 27 18:14:02 2021 +0200
1.3 @@ -291,7 +291,7 @@
1.4 SOME (rew, _) => rew
1.5 | NONE => raise ERROR ""
1.6 in SOME (rew, (thmID, thm)) end)
1.7 - handle _ (*TODO Pattern.MATCH ?del?*)=> raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
1.8 + handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
1.9 end;
1.10
1.11 fun eval_prog_expr thy srls t =