--- 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;
--- 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;