# HG changeset patch
# User wenzelm
# Date 1185712204 -7200
# Node ID a12b4faff474bb21431e86329e9d308a4a5064f5
# Parent  47b588ce11ec06a9e42bea38b8c385d3460430ae
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
moved Drule.is_dummy_thm to Thm.is_dummy;

diff -r 47b588ce11ec -r a12b4faff474 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Jul 29 14:30:03 2007 +0200
+++ b/src/Pure/drule.ML	Sun Jul 29 14:30:04 2007 +0200
@@ -93,9 +93,6 @@
   val store_thm_open: bstring -> thm -> thm
   val store_standard_thm_open: bstring -> thm -> thm
   val compose_single: thm * int * thm -> thm
-  val add_rule: thm -> thm list -> thm list
-  val del_rule: thm -> thm list -> thm list
-  val merge_rules: thm list * thm list -> thm list
   val imp_cong_rule: thm -> thm -> thm
   val arg_cong_rule: cterm -> thm -> thm
   val binop_cong_rule: cterm -> thm -> thm -> thm
@@ -119,7 +116,6 @@
   val cterm_rule: (thm -> thm) -> cterm -> cterm
   val term_rule: theory -> (thm -> thm) -> term -> term
   val dummy_thm: thm
-  val is_dummy_thm: thm -> bool
   val sort_triv: theory -> typ * sort -> thm list
   val unconstrainTs: thm -> thm
   val with_subgoal: int -> (thm -> thm) -> thm -> thm
@@ -518,11 +514,6 @@
 (*Useful "distance" function for BEST_FIRST*)
 val size_of_thm = size_of_term o Thm.full_prop_of;
 
-(*maintain lists of theorems --- preserving canonical order*)
-val del_rule = remove Thm.eq_thm_prop;
-fun add_rule th = cons th o del_rule th;
-val merge_rules = Library.merge Thm.eq_thm_prop;
-
 
 
 (*** Meta-Rewriting Rules ***)
@@ -895,16 +886,7 @@
 fun cterm_rule f = dest_term o f o mk_term;
 fun term_rule thy f t = Thm.term_of (cterm_rule f (Thm.cterm_of thy t));
 
-
-(* dummy_thm *)
-
-val dummy_prop = Term.dummy_pattern propT;
-val dummy_thm = mk_term (Thm.cterm_of ProtoPure.thy dummy_prop);
-
-fun is_dummy_thm th =
-  (case try dest_term th of
-    NONE => false
-  | SOME ct => Logic.strip_imp_concl (Thm.term_of ct) aconv dummy_prop);
+val dummy_thm = mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT));
 
 
 
diff -r 47b588ce11ec -r a12b4faff474 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Jul 29 14:30:03 2007 +0200
+++ b/src/Pure/more_thm.ML	Sun Jul 29 14:30:04 2007 +0200
@@ -27,8 +27,12 @@
   val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val equiv_thm: thm * thm -> bool
+  val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
+  val add_thm: thm -> thm list -> thm list
+  val del_thm: thm -> thm list -> thm list
+  val merge_thms: thm list * thm list -> thm list
   val axiomK: string
   val assumptionK: string
   val definitionK: string
@@ -136,6 +140,11 @@
 
 (* misc operations *)
 
+fun is_dummy thm =
+  (case try Logic.dest_term (Thm.concl_of thm) of
+    NONE => false
+  | SOME t => Term.is_dummy_pattern t);
+
 fun plain_prop_of raw_thm =
   let
     val thm = Thm.strip_shyps raw_thm;
@@ -156,6 +165,13 @@
   in fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps end;
 
 
+(* lists of theorems in canonical order *)
+
+val add_thm = update eq_thm_prop;
+val del_thm = remove eq_thm_prop;
+val merge_thms = merge eq_thm_prop;
+
+
 
 (** theorem kinds **)