src/Pure/Isar/locale.ML
changeset 19873 588329441a78
parent 19810 dae765e552ce
child 19900 21a99d88d925
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Jun 13 15:42:52 2006 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Jun 13 23:41:31 2006 +0200
     1.3 @@ -1961,7 +1961,7 @@
     1.4        Attrib.attribute_i Drule.standard
     1.5        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
     1.6        (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
     1.7 -        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.freeze_all th))
     1.8 +        Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, Drule.unvarify th))
     1.9          (* FIXME *)) x;
    1.10  
    1.11  fun local_activate_facts_elemss x = gen_activate_facts_elemss