--- a/TFL/rules.ML Fri Sep 28 19:23:07 2001 +0200
+++ b/TFL/rules.ML Fri Sep 28 19:23:35 2001 +0200
@@ -57,7 +57,7 @@
-> thm -> thm * term list
val RIGHT_ASSOC : thm -> thm
- val prove : cterm * tactic -> thm
+ val prove : bool -> cterm * tactic -> thm
end;
structure Rules: RULES =
@@ -813,11 +813,13 @@
end;
-fun prove (ptm, tac) =
+fun prove strict (ptm, tac) =
let val result =
- Library.transform_error (fn () =>
- Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
- handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg)
+ if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
+ else
+ Library.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;