# HG changeset patch # User ballarin # Date 1219852471 -7200 # Node ID d1c2fa105443ec8a6d3bb42d1ec1bcbe2d87a680 # Parent 92dd3ad302b7884d1de5f3e5e5e0b3874e7eca3e Consistent naming of theorems in interpretation. diff -r 92dd3ad302b7 -r d1c2fa105443 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Aug 27 16:32:48 2008 +0200 +++ b/src/Pure/Isar/locale.ML Wed Aug 27 17:54:31 2008 +0200 @@ -1571,19 +1571,21 @@ (* naming of interpreted theorems *) -fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy = +fun global_note_prefix_i kind loc (fully_qualified, prfx) params args thy = thy |> Sign.qualified_names |> Sign.add_path (NameSpace.base loc ^ "_locale") |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx) + |> (if fully_qualified then Sign.add_path (space_implode "_" params) else I) |> PureThy.note_thmss kind args ||> Sign.restore_naming thy; -fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt = +fun local_note_prefix_i kind loc (fully_qualified, prfx) params args ctxt = ctxt |> ProofContext.qualified_names |> ProofContext.add_path (NameSpace.base loc ^ "_locale") |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx) + |> (if fully_qualified then ProofContext.add_path (space_implode "_" params) else I) |> ProofContext.note_thmss_i kind args ||> ProofContext.restore_naming ctxt; @@ -1642,8 +1644,6 @@ in Element.facts_map (Element.morph_ctxt morphism) facts end; -(* suppress application of name morphism: workaroud for class package *) (* FIXME *) - fun morph_ctxt' phi = Element.map_ctxt {name = I, var = Morphism.var phi, @@ -1658,11 +1658,13 @@ fun interpret_args thy prfx insts prems eqns atts2 exp attrib args = let val inst = Morphism.name_morphism (NameSpace.qualified prfx) $> +(* need to add parameter prefix *) (* FIXME *) Element.inst_morphism thy insts $> Element.satisfy_morphism prems $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) in args |> Element.facts_map (morph_ctxt' inst) |> +(* suppresses application of name morphism: workaroud for class package *) (* FIXME *) map (fn (attn, bs) => (attn, bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |> standardize thy exp |> Attrib.map_facts attrib @@ -1686,7 +1688,7 @@ val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts; val attrib = Attrib.attribute_i thy; val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args; - in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end; + in global_note_prefix_i kind target (fully_qualified, prfx) (map fst parms) args' thy |> snd end; in fold activate regs thy end; @@ -2089,7 +2091,7 @@ val facts' = interpret_args (ProofContext.theory_of ctxt) prfx (Symtab.empty, Symtab.empty) prems eqns atts exp (attrib thy_ctxt) facts; - in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end + in snd (note_interp kind loc (fully_qualified, prfx) [] facts' thy_ctxt) end | activate_elem _ _ _ _ thy_ctxt = thy_ctxt; fun activate_elems all_eqns ((id, _), elems) thy_ctxt = @@ -2376,7 +2378,7 @@ |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) in thy - |> global_note_prefix_i kind loc (fully_qualified, prfx) facts' + |> global_note_prefix_i kind loc (fully_qualified, prfx) [] facts' |> snd end | activate_elem _ _ thy = thy;