use Drule.unvarify instead of obsolete Drule.freeze_all;
authorwenzelm
Tue Jun 13 23:41:31 2006 +0200 (2006-06-13)
changeset 19873588329441a78
parent 19872 1b53b196f85f
child 19874 cc4b2b882e4c
use Drule.unvarify instead of obsolete Drule.freeze_all;
src/HOL/Import/proof_kernel.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Jun 13 15:42:52 2006 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Jun 13 23:41:31 2006 +0200
     1.3 @@ -2029,7 +2029,7 @@
     1.4  				 names'
     1.5  				 (thy1,th)
     1.6  	    val _ = ImportRecorder.add_specification names' th
     1.7 -	    val res' = Drule.freeze_all res
     1.8 +	    val res' = Drule.unvarify res
     1.9  	    val hth = HOLThm(rens,res')
    1.10  	    val rew = rewrite_hol4_term (concl_of res') thy'
    1.11  	    val th  = equal_elim rew res'
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Jun 13 15:42:52 2006 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Jun 13 23:41:31 2006 +0200
     2.3 @@ -1961,7 +1961,7 @@
     2.4        Attrib.attribute_i Drule.standard
     2.5        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
     2.6        (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
     2.7 -        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.freeze_all th))
     2.8 +        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.unvarify th))
     2.9          (* FIXME *)) x;
    2.10  
    2.11  fun local_activate_facts_elemss x = gen_activate_facts_elemss