# HG changeset patch
# User wenzelm
# Date 1085836025 -7200
# Node ID ba0fc27a6c7ed6c67d692c69eae9b99bc08b2421
# Parent  695ee8ad0bb6fc30163d88347689107db5b42ca0
transform_error;

diff -r 695ee8ad0bb6 -r ba0fc27a6c7e TFL/rules.ML
--- 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;
diff -r 695ee8ad0bb6 -r ba0fc27a6c7e src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sat May 29 15:06:42 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sat May 29 15:07:05 2004 +0200
@@ -343,8 +343,8 @@
         val check =
           (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
             fn _ => fn thm => rule := Some thm) true state))
-          |> Library.setmp proofs 0
-          |> Library.transform_error;
+          |> setmp proofs 0
+          |> transform_error;
         val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
       in (case result of (Some _, None) => () | (_, exn) => fail exn); state end;