--- 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;