# HG changeset patch # User ballarin # Date 1190134217 -7200 # Node ID 69cb317edf73028bddada1308762b8b2674f4fdd # Parent 4d1876424529da5ce87b472650a18886cf369d55 Morphisms applied in global interpretations behave correctly on types and terms. diff -r 4d1876424529 -r 69cb317edf73 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Sep 18 18:49:17 2007 +0200 +++ b/src/Pure/Isar/locale.ML Tue Sep 18 18:50:17 2007 +0200 @@ -1596,7 +1596,10 @@ val eqns = fold_map (join_eqns (get_global_registration thy) I (ProofContext.init thy)) ids' Termtab.empty |> snd |> Termtab.dest |> map snd; - in ((tinst, inst), wits, eqns) end; + + val tinst' = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of vts) Vartab.empty + |> Vartab.dest |> map (fn ((x, 0), (_, T)) => (x, T)) |> Symtab.make; + in ((tinst', vinst), (tinst, inst), wits, eqns) end; (* store instantiations of args for all registered interpretations @@ -1614,11 +1617,11 @@ fun activate (vts, (((fully_qualified, prfx), atts2), _, _)) thy = let - val (insts, prems, eqns) = collect_global_witnesses thy parms ids vts; + val (vinsts, insts, prems, eqns) = collect_global_witnesses thy parms ids vts; val attrib = Attrib.attribute_i thy; val inst_atts = Args.morph_values (Morphism.name_morphism (NameSpace.qualified prfx) $> - Element.inst_morphism thy insts $> + Element.inst_morphism' thy vinsts insts $> Element.satisfy_morphism prems $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns #> Drule.standard)); @@ -2301,7 +2304,7 @@ fun activate_reg (vts, (((fully_qualified, prfx), atts2), _, _)) thy = let - val (insts, wits, _) = collect_global_witnesses thy fixed target_ids vts; + val (vinsts, insts, wits, _) = collect_global_witnesses thy fixed target_ids vts; fun inst_parms ps = map (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; val disch = Element.satisfy_thm wits; @@ -2316,7 +2319,7 @@ else thy |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) |> fold (fn witn => fn thy => add_global_witness (name, ps') - (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms + (Element.morph_witness (Element.inst_morphism' thy vinsts insts) witn) thy) thms end; fun activate_derived_id ((_, Assumed _), _) thy = thy