--- a/src/HOL/HOL.thy Fri Apr 23 19:32:37 2010 +0200
+++ b/src/HOL/HOL.thy Fri Apr 23 19:36:23 2010 +0200
@@ -30,7 +30,6 @@
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
"~~/src/Tools/more_conv.ML"
- "~~/src/HOL/Tools/Sledgehammer/named_thm_set.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -801,7 +800,7 @@
*}
ML {*
-structure No_ATPs = Named_Thm_Set
+structure No_ATPs = Named_Thms
(
val name = "no_atp"
val description = "theorems that should be filtered out by Sledgehammer"
--- a/src/HOL/IsaMakefile Fri Apr 23 19:32:37 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 23 19:36:23 2010 +0200
@@ -136,7 +136,6 @@
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
HOL.thy \
- Tools/Sledgehammer/named_thm_set.ML \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
Tools/simpdata.ML
--- a/src/HOL/Tools/Sledgehammer/named_thm_set.ML Fri Apr 23 19:32:37 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/named_thm_set.ML
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Named sets of theorems.
-*)
-
-signature NAMED_THM_SET =
-sig
- val member: Proof.context -> thm -> bool
- val add_thm: thm -> Context.generic -> Context.generic
- val del_thm: thm -> Context.generic -> Context.generic
- val add: attribute
- val del: attribute
- val setup: theory -> theory
-end;
-
-functor Named_Thm_Set(val name: string val description: string)
- : NAMED_THM_SET =
-struct
-
-structure Data = Generic_Data
-(
- type T = thm Termtab.table;
- val empty = Termtab.empty;
- val extend = I;
- fun merge tabs = Termtab.merge (K true) tabs;
-);
-
-fun member ctxt th =
- Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
-
-fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
-fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
-
-val add = Thm.declaration_attribute add_thm;
-val del = Thm.declaration_attribute del_thm;
-
-val setup =
- Attrib.setup (Binding.name name) (Attrib.add_del add del)
- ("declaration of " ^ description) #>
- PureThy.add_thms_dynamic (Binding.name name,
- map #2 o Termtab.dest o Data.get);
-
-end;
--- a/src/Pure/Tools/named_thms.ML Fri Apr 23 19:32:37 2010 +0200
+++ b/src/Pure/Tools/named_thms.ML Fri Apr 23 19:36:23 2010 +0200
@@ -6,6 +6,7 @@
signature NAMED_THMS =
sig
+ val member: Proof.context -> thm -> bool
val get: Proof.context -> thm list
val add_thm: thm -> Context.generic -> Context.generic
val del_thm: thm -> Context.generic -> Context.generic
@@ -25,6 +26,8 @@
val merge = Item_Net.merge;
);
+val member = Item_Net.member o Data.get o Context.Proof;
+
val content = Item_Net.content o Data.get;
val get = content o Context.Proof;
--- a/src/Pure/item_net.ML Fri Apr 23 19:32:37 2010 +0200
+++ b/src/Pure/item_net.ML Fri Apr 23 19:36:23 2010 +0200
@@ -11,6 +11,7 @@
val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
val content: 'a T -> 'a list
val retrieve: 'a T -> term -> 'a list
+ val member: 'a T -> 'a -> bool
val merge: 'a T * 'a T -> 'a T
val remove: 'a -> 'a T -> 'a T
val update: 'a -> 'a T -> 'a T
@@ -49,7 +50,6 @@
mk_items eq index (x :: content) (next - 1)
(fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
-
fun merge (items1, Items {content = content2, ...}) =
fold_rev (fn y => if member items1 y then I else cons y) content2 items1;