src/Provers/hypsubst.ML
changeset 20974 2a29a21825d1
parent 20945 1de0d565b483
child 21221 ef30d1e6f03a
     1.1 --- a/src/Provers/hypsubst.ML	Wed Oct 11 14:51:24 2006 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Wed Oct 11 14:51:25 2006 +0200
     1.3 @@ -34,8 +34,8 @@
     1.4  signature HYPSUBST_DATA =
     1.5    sig
     1.6    val dest_Trueprop    : term -> term
     1.7 -  val dest_eq          : term -> term*term*typ
     1.8 -  val dest_imp         : term -> term*term
     1.9 +  val dest_eq          : term -> (term * term) *typ
    1.10 +  val dest_imp         : term -> term * term
    1.11    val eq_reflection    : thm               (* a=b ==> a==b *)
    1.12    val rev_eq_reflection: thm               (* a==b ==> a=b *)
    1.13    val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    1.14 @@ -55,7 +55,7 @@
    1.15    val gen_hyp_subst_tac      : bool -> int -> tactic
    1.16    val vars_gen_hyp_subst_tac : bool -> int -> tactic
    1.17    val eq_var                 : bool -> bool -> term -> int * bool
    1.18 -  val inspect_pair           : bool -> bool -> term * term * typ -> bool
    1.19 +  val inspect_pair           : bool -> bool -> (term * term) * typ -> bool
    1.20    val mk_eqs                 : bool -> thm -> thm list
    1.21    val stac                   : thm -> int -> tactic
    1.22    val hypsubst_setup         : theory -> theory
    1.23 @@ -89,7 +89,7 @@
    1.24          but we can't check for this -- hence bnd and bound_hyp_subst_tac
    1.25    Prefer to eliminate Bound variables if possible.
    1.26    Result:  true = use as is,  false = reorient first *)
    1.27 -fun inspect_pair bnd novars (t,u,T) =
    1.28 +fun inspect_pair bnd novars ((t, u), T) =
    1.29    if novars andalso maxidx_of_typ T <> ~1
    1.30    then raise Match   (*variables in the type!*)
    1.31    else