# HG changeset patch
# User wenzelm
# Date 1114716947 -7200
# Node ID 3e9a54e033b975f71271f8193bbb89e43baa7198
# Parent  6236cc88d4b8beb367fea60b326545744f4f0542
added plain_prop_of;

diff -r 6236cc88d4b8 -r 3e9a54e033b9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Apr 28 21:35:25 2005 +0200
+++ b/src/Pure/drule.ML	Thu Apr 28 21:35:47 2005 +0200
@@ -88,6 +88,7 @@
   include BASIC_DRULE
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
+  val plain_prop_of: thm -> term
   val add_used: thm -> string list -> string list
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
   val tag_rule: tag -> thm -> thm
@@ -221,6 +222,22 @@
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
+fun plain_prop_of raw_thm =
+  let
+    val thm = Thm.strip_shyps raw_thm;
+    fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
+    val {hyps, prop, tpairs, ...} = Thm.rep_thm thm;
+  in
+    if not (null hyps) then
+      err "theorem may not contain hypotheses"
+    else if not (null (Thm.extra_shyps thm)) then
+      err "theorem may not contain sort hypotheses"
+    else if not (null tpairs) then
+      err "theorem may not contain flex-flex pairs"
+    else prop
+  end;
+
+
 
 (** reading of instantiations **)