# HG changeset patch
# User wenzelm
# Date 1450778285 -3600
# Node ID 3f5e2e0a6d29d09fd5d04730570aae6c45091353
# Parent  77fa1ae5fd31e6290396fc2130a896b3d94f3b0c
tuned;

diff -r 77fa1ae5fd31 -r 3f5e2e0a6d29 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 10:35:35 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 22 10:58:05 2015 +0100
@@ -182,19 +182,10 @@
     |> Method.local_setup binding (Scan.succeed get_method) "(internal)"
   end;
 
-(* FIXME: In general we need the ability to override all dynamic facts.
-   This is also slow: we need Named_Theorems.only *)
-fun empty_named_thm named_thm ctxt =
-  let
-    val contents = Named_Theorems.get ctxt named_thm;
-    val attrib = snd oo Thm.proof_attributes [Named_Theorems.del named_thm];
-  in fold attrib contents ctxt end;
-
-fun dummy_named_thm named_thm ctxt =
-  let
-    val ctxt' = empty_named_thm named_thm ctxt;
-    val (_, ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] Drule.free_dummy_thm ctxt';
-  in ctxt'' end;
+fun dummy_named_thm named_thm =
+  Context.proof_map
+    (Named_Theorems.clear named_thm
+      #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm);
 
 fun parse_method_args method_names =
   let
@@ -277,7 +268,7 @@
       (parse_term_args args --
         parse_method_args method_names --|
         (Scan.depend (fn context =>
-              Scan.succeed (Context.map_proof (fold empty_named_thm uses_internal) context, ())) --
+          Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) --
          Method.sections modifiers) >> eval);
 
     val lthy3 = lthy2
diff -r 77fa1ae5fd31 -r 3f5e2e0a6d29 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Tue Dec 22 10:35:35 2015 +0100
+++ b/src/Pure/Tools/named_theorems.ML	Tue Dec 22 10:58:05 2015 +0100
@@ -8,6 +8,7 @@
 sig
   val member: Proof.context -> string -> thm -> bool
   val get: Proof.context -> string -> thm list
+  val clear: string -> Context.generic -> Context.generic
   val add_thm: string -> thm -> Context.generic -> Context.generic
   val del_thm: string -> thm -> Context.generic -> Context.generic
   val add: string -> attribute
@@ -55,6 +56,8 @@
 
 val get = content o Context.Proof;
 
+fun clear name = map_entry name (K Thm.full_rules);
+
 fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
 fun del_thm name = map_entry name o Item_Net.remove;