# HG changeset patch
# User wenzelm
# Date 1154007201 -7200
# Node ID 7e17d70a93039a8068d315c5fad5b1542526d7dd
# Parent  5daab2c78b8ec4996eb651153610901ac9710b74
eliminated obsolete freeze_thaw;

diff -r 5daab2c78b8e -r 7e17d70a9303 TFL/rules.ML
--- 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;
diff -r 5daab2c78b8e -r 7e17d70a9303 src/Pure/conjunction.ML
--- 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