# HG changeset patch
# User wenzelm
# Date 1150234891 -7200
# Node ID 588329441a7885f32eede668d70e67dafa2377b9
# Parent  1b53b196f85f0675d7d17985cd0fb474759996e5
use Drule.unvarify instead of obsolete Drule.freeze_all;

diff -r 1b53b196f85f -r 588329441a78 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Tue Jun 13 15:42:52 2006 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Jun 13 23:41:31 2006 +0200
@@ -2029,7 +2029,7 @@
 				 names'
 				 (thy1,th)
 	    val _ = ImportRecorder.add_specification names' th
-	    val res' = Drule.freeze_all res
+	    val res' = Drule.unvarify res
 	    val hth = HOLThm(rens,res')
 	    val rew = rewrite_hol4_term (concl_of res') thy'
 	    val th  = equal_elim rew res'
diff -r 1b53b196f85f -r 588329441a78 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jun 13 15:42:52 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jun 13 23:41:31 2006 +0200
@@ -1961,7 +1961,7 @@
       Attrib.attribute_i Drule.standard
       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
       (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
-        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.freeze_all th))
+        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.unvarify th))
         (* FIXME *)) x;
 
 fun local_activate_facts_elemss x = gen_activate_facts_elemss