# HG changeset patch
# User wenzelm
# Date 1185559908 -7200
# Node ID 2d473ed154914763cc3096e19aa812fcfe2afc6d
# Parent  8c962a9be9f2fe7ce688d08ede94d787e3728d0f
added dummy_thm, is_dummy_thm;

diff -r 8c962a9be9f2 -r 2d473ed15491 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jul 27 20:11:47 2007 +0200
+++ b/src/Pure/drule.ML	Fri Jul 27 20:11:48 2007 +0200
@@ -118,6 +118,8 @@
   val dest_term: thm -> cterm
   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
@@ -894,6 +896,17 @@
 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);
+
+
 
 (** variations on instantiate **)