# HG changeset patch
# User ballarin
# Date 1238340137 -7200
# Node ID 7fb900cad123e3975db20039a33ae728816fd300
# Parent  c3f1e8a9e0b56545fbef4c5afdc70a5ba0637773
Normalise equation only for morphism, not thm stored in theory.

diff -r c3f1e8a9e0b5 -r 7fb900cad123 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Mar 28 22:14:21 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Mar 29 17:22:17 2009 +0200
@@ -833,10 +833,10 @@
                Locale.activate_global_facts (name, morph $> export)) regs
       | store_eqns_activate regs eqs thy =
           let
-            val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
-              LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+            val eqs' = eqs |> map (Morphism.thm (export' $> export));
+            val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
               Drule.abs_def);
-            val eq_morph = Element.eq_morphism thy eqs';
+            val eq_morph = Element.eq_morphism thy morph_eqs;
             val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
           in
             thy