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