src/Pure/Isar/expression.ML
changeset 30781 7fb900cad123
parent 30725 c23a5b3cd1b9
child 30783 275577cefaa8
     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