TFL/rules.ML
changeset 14836 ba0fc27a6c7e
parent 14643 130076a81b84
child 15011 35be762f58f9
--- a/TFL/rules.ML	Sat May 29 15:06:42 2004 +0200
+++ b/TFL/rules.ML	Sat May 29 15:07:05 2004 +0200
@@ -817,7 +817,7 @@
   let val result =
     if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
     else
-      Library.transform_error (fn () =>
+      transform_error (fn () =>
         Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
       handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
   in #1 (freeze_thaw result) end;