# HG changeset patch # User wenzelm # Date 1407693210 -7200 # Node ID 9c193dcc8ec80a8202ccb8808ec68a607eb1823e # Parent 44354c99d75405b19d1366bcfc89813d9ac0a989 some localization; diff -r 44354c99d754 -r 9c193dcc8ec8 src/Pure/Tools/named_theorems.ML --- a/src/Pure/Tools/named_theorems.ML Sun Aug 10 19:44:20 2014 +0200 +++ b/src/Pure/Tools/named_theorems.ML Sun Aug 10 19:53:30 2014 +0200 @@ -12,7 +12,7 @@ val del_thm: string -> thm -> Context.generic -> Context.generic val add: string -> attribute val del: string -> attribute - val declare: binding -> string -> theory -> string * theory + val declare: binding -> string -> local_theory -> string * local_theory end; structure Named_Theorems: NAMED_THEOREMS = @@ -59,27 +59,34 @@ (* declaration *) -fun declare binding descr thy = +fun declare binding descr lthy = let - (* FIXME proper result from Global_Theory.add_thms_dynamic *) - val naming = Name_Space.naming_of (Context.Theory thy); - val name = Name_Space.full_name naming binding; - - val thy' = thy - |> Global_Theory.add_thms_dynamic (binding, fn context => content context name); - + val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding; val description = "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); - val thy'' = thy' - |> Context.theory_map (new_entry name) - |> Attrib.setup binding (Attrib.add_del (add name) (del name)) description; - in (name, thy'') end; + val lthy' = lthy + |> Local_Theory.background_theory + (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #> + Attrib.setup binding (Attrib.add_del (add name) (del name)) description #> + Context.theory_map (new_entry name)) + |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) + |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => + let + val binding' = Morphism.binding phi binding; + val context' = + context |> Context.mapping + (Global_Theory.alias_fact binding' name) + (fn ctxt => + if Facts.defined (Proof_Context.facts_of ctxt) name + then Proof_Context.fact_alias binding' name ctxt + else ctxt); + in context' end); + in (name, lthy') end; val _ = - Outer_Syntax.command @{command_spec "named_theorems"} + Outer_Syntax.local_theory @{command_spec "named_theorems"} "declare named collection of theorems" - (Parse.binding -- Scan.optional Parse.text "" - >> (fn (binding, descr) => Toplevel.theory (snd o declare binding descr))); + (Parse.binding -- Scan.optional Parse.text "" >> (fn (b, descr) => snd o declare b descr)); (* ML antiquotation *)