Normalise equation only for morphism, not thm stored in theory.
authorballarin
Sun Mar 29 17:22:17 2009 +0200 (2009-03-29)
changeset 307817fb900cad123
parent 30780 c3f1e8a9e0b5
child 30782 38e477e8524f
Normalise equation only for morphism, not thm stored in theory.
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 28 22:14:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 17:22:17 2009 +0200
     1.3 @@ -833,10 +833,10 @@
     1.4                 Locale.activate_global_facts (name, morph $> export)) regs
     1.5        | store_eqns_activate regs eqs thy =
     1.6            let
     1.7 -            val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
     1.8 -              LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
     1.9 +            val eqs' = eqs |> map (Morphism.thm (export' $> export));
    1.10 +            val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
    1.11                Drule.abs_def);
    1.12 -            val eq_morph = Element.eq_morphism thy eqs';
    1.13 +            val eq_morph = Element.eq_morphism thy morph_eqs;
    1.14              val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
    1.15            in
    1.16              thy