src/Pure/drule.ML
changeset 1703 e22ad43bab5f
parent 1596 4a09f4698813
child 1756 978ee7ededdd
     1.1 --- a/src/Pure/drule.ML	Tue Apr 30 11:08:09 1996 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Apr 30 12:03:01 1996 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    val forall_elim_vars	: int -> thm -> thm
     1.5    val implies_elim_list	: thm -> thm list -> thm
     1.6    val implies_intr_list	: cterm list -> thm -> thm
     1.7 +  val dest_cimplies     : cterm -> cterm * cterm
     1.8    val MRL		: thm list list * thm list -> thm list
     1.9    val MRS		: thm list * thm -> thm
    1.10    val read_instantiate	: (string*string)list -> thm -> thm
    1.11 @@ -192,6 +193,17 @@
    1.12  
    1.13  (** some cterm->cterm operations: much faster than calling cterm_of! **)
    1.14  
    1.15 +(*dest_implies for cterms. Note T=prop below*)
    1.16 +fun dest_cimplies ct =
    1.17 +  (let val (ct1, ct2) = dest_comb ct
    1.18 +       val {t, ...} = rep_cterm ct1;
    1.19 +   in case head_of t of
    1.20 +          Const("==>", _) => (snd (dest_comb ct1), ct2)
    1.21 +        | _ => raise TERM ("dest_cimplies", [term_of ct])
    1.22 +   end
    1.23 +  ) handle CTERM "dest_comb" => raise TERM ("dest_cimplies", [term_of ct]);
    1.24 +
    1.25 +
    1.26  (*Discard flexflex pairs; return a cterm*)
    1.27  fun cskip_flexpairs ct =
    1.28      case term_of ct of
    1.29 @@ -511,7 +523,7 @@
    1.30  (*Do not rewrite flex-flex pairs*)
    1.31  fun goals_conv pred cv =
    1.32    let fun gconv i ct =
    1.33 -        let val (A,B) = Thm.dest_cimplies ct
    1.34 +        let val (A,B) = dest_cimplies ct
    1.35              val (thA,j) = case term_of A of
    1.36                    Const("=?=",_)$_$_ => (reflexive A, i)
    1.37                  | _ => (if pred i then cv A else reflexive A, i+1)