src/Tools/isac/MathEngBasic/rewrite.sml
changeset 60263 95bae6eeccfa
parent 60262 aa0f0bf98d40
child 60267 a3ee0a3cedba
     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 =