added plain_prop_of;
authorwenzelm
Thu Apr 28 21:35:47 2005 +0200 (2005-04-28)
changeset 158753e9a54e033b9
parent 15874 6236cc88d4b8
child 15876 a67343c6ab2a
added plain_prop_of;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Thu Apr 28 21:35:25 2005 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Apr 28 21:35:47 2005 +0200
     1.3 @@ -88,6 +88,7 @@
     1.4    include BASIC_DRULE
     1.5    val strip_comb: cterm -> cterm * cterm list
     1.6    val strip_type: ctyp -> ctyp list * ctyp
     1.7 +  val plain_prop_of: thm -> term
     1.8    val add_used: thm -> string list -> string list
     1.9    val rule_attribute: ('a -> thm -> thm) -> 'a attribute
    1.10    val tag_rule: tag -> thm -> thm
    1.11 @@ -221,6 +222,22 @@
    1.12        in (cT1 :: cTs, cT') end
    1.13    | _ => ([], cT));
    1.14  
    1.15 +fun plain_prop_of raw_thm =
    1.16 +  let
    1.17 +    val thm = Thm.strip_shyps raw_thm;
    1.18 +    fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
    1.19 +    val {hyps, prop, tpairs, ...} = Thm.rep_thm thm;
    1.20 +  in
    1.21 +    if not (null hyps) then
    1.22 +      err "theorem may not contain hypotheses"
    1.23 +    else if not (null (Thm.extra_shyps thm)) then
    1.24 +      err "theorem may not contain sort hypotheses"
    1.25 +    else if not (null tpairs) then
    1.26 +      err "theorem may not contain flex-flex pairs"
    1.27 +    else prop
    1.28 +  end;
    1.29 +
    1.30 +
    1.31  
    1.32  (** reading of instantiations **)
    1.33