use Drule.unvarify instead of obsolete Drule.freeze_all;

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

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