--- a/TFL/rules.ML Thu Jul 27 14:21:57 2006 +0200
+++ b/TFL/rules.ML Thu Jul 27 15:33:21 2006 +0200
@@ -816,10 +816,11 @@
fun prove strict (ptm, tac) =
let
val {thy, t, ...} = Thm.rep_cterm ptm;
- val result =
- if strict then Goal.prove_global thy [] [] t (K tac)
- else Goal.prove_global thy [] [] t (K tac)
- handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg);
- in #1 (freeze_thaw result) end;
+ val ctxt = ProofContext.init thy |> ProofContext.fix_frees t;
+ in
+ if strict then Goal.prove ctxt [] [] t (K tac)
+ else Goal.prove ctxt [] [] t (K tac)
+ handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
+ end;
end;
--- a/src/Pure/conjunction.ML Thu Jul 27 14:21:57 2006 +0200
+++ b/src/Pure/conjunction.ML Thu Jul 27 15:33:21 2006 +0200
@@ -74,7 +74,7 @@
val ABC = read "PROP A ==> PROP B ==> PROP C";
val A_B = read "PROP ProtoPure.conjunction(A, B)"
-val conjunction_def = #1 (freeze_thaw ProtoPure.conjunction_def);
+val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
fun conjunctionD which =
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP