# 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 **)