# 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 *)