# HG changeset patch
# User haftmann
# Date 1555520226 0
# Node ID ca9dfa7ee3bd1a60eb11cf1cf0449311bf3f9915
# Parent  93516cb6cd3080cbe184ee01855d5d5f85c80c77
backed out experimental b67bab2b132c, which slipped in accidentally

diff -r 93516cb6cd30 -r ca9dfa7ee3bd src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Thu Apr 18 06:19:30 2019 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Apr 17 16:57:06 2019 +0000
@@ -182,7 +182,7 @@
       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
       |> Config.put Method.old_section_parser true
       |> fold setup_local_method methods
-      |> fold_map (fn b => Named_Theorems.declare b [] "") uses;
+      |> fold_map (fn b => Named_Theorems.declare b "") uses;
 
     val (term_args, lthy2) = lthy1
       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
diff -r 93516cb6cd30 -r ca9dfa7ee3bd src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 18 06:19:30 2019 +0200
+++ b/src/Pure/Pure.thy	Wed Apr 17 16:57:06 2019 +0000
@@ -545,9 +545,8 @@
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
     "declare named collection of theorems"
-    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text ""
-      -- Scan.optional (\<^keyword>\<open>includes\<close> |-- Scan.repeat1 Parse.text) []) >>
-      fold (fn ((b, descr), extends) => snd o Named_Theorems.declare b extends descr));
+    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
+      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
 
 in end\<close>
 
diff -r 93516cb6cd30 -r ca9dfa7ee3bd src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Thu Apr 18 06:19:30 2019 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Wed Apr 17 16:57:06 2019 +0000
@@ -14,8 +14,7 @@
   val add: string -> attribute
   val del: string -> attribute
   val check: Proof.context -> string * Position.T -> string
-  val declare: binding -> string list -> string ->
-    local_theory -> string * local_theory
+  val declare: binding -> string -> local_theory -> string * local_theory
 end;
 
 structure Named_Theorems: NAMED_THEOREMS =
@@ -88,17 +87,15 @@
 
 (* declaration *)
 
-fun declare binding raw_extends descr lthy =
+fun declare binding descr lthy =
   let
     val name = Local_Theory.full_name lthy binding;
-    val extends = map (fn s => check lthy (s, Position.none)) raw_extends;
     val description =
       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
     val lthy' = lthy
       |> Local_Theory.background_theory (Context.theory_map (new_entry name))
       |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
-      |> Local_Theory.add_thms_dynamic (binding,
-           fn context => maps (content context) (extends @ [name]))
+      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
   in (name, lthy') end;
 
diff -r 93516cb6cd30 -r ca9dfa7ee3bd src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Thu Apr 18 06:19:30 2019 +0200
+++ b/src/Tools/atomize_elim.ML	Wed Apr 17 16:57:06 2019 +0000
@@ -19,7 +19,7 @@
 val named_theorems =
   Context.>>> (Context.map_theory_result
    (Named_Target.theory_init #>
-    Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> [] "atomize_elim rewrite rule" ##>
+    Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> "atomize_elim rewrite rule" ##>
     Local_Theory.exit_global));