# HG changeset patch # User wenzelm # Date 1164402319 -3600 # Node ID a267ecd51f90f25e6277b16b67f0e3351bcdf74e # Parent bd641d92743711f29b71796b9633feab5837ad70 tuned morphisms; diff -r bd641d927437 -r a267ecd51f90 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Nov 24 22:05:18 2006 +0100 +++ b/src/Pure/Isar/locale.ML Fri Nov 24 22:05:19 2006 +0100 @@ -2155,13 +2155,14 @@ fun activate_elem (Notes (kind, facts)) thy = let - val att_morphism = Morphism.morphism {var = I, name = I, - typ = Element.instT_type (#1 insts), term = Element.inst_term insts, - thm = disch o Element.inst_thm thy insts o satisfy}; + val att_morphism = + Morphism.thm_morphism satisfy $> + Element.inst_morphism thy insts $> + Morphism.thm_morphism disch; val facts' = facts - |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) - |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2))) - |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) + |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) + |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2))) + |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) in thy |> global_note_prefix_i kind prfx facts'