src/Pure/term.ML
changeset 35227 d67857e3a8c0
parent 34922 e35f608f81a2
child 35986 b7fcca3d9a44
     1.1 --- a/src/Pure/term.ML	Fri Feb 19 11:06:21 2010 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Feb 19 11:06:22 2010 +0100
     1.3 @@ -45,6 +45,7 @@
     1.4    val dest_Const: term -> string * typ
     1.5    val dest_Free: term -> string * typ
     1.6    val dest_Var: term -> indexname * typ
     1.7 +  val dest_comb: term -> term * term
     1.8    val domain_type: typ -> typ
     1.9    val range_type: typ -> typ
    1.10    val binder_types: typ -> typ list
    1.11 @@ -278,6 +279,9 @@
    1.12  fun dest_Var (Var x) =  x
    1.13    | dest_Var t = raise TERM("dest_Var", [t]);
    1.14  
    1.15 +fun dest_comb (t1 $ t2) = (t1, t2)
    1.16 +  | dest_comb t = raise TERM("dest_comb", [t]);
    1.17 +
    1.18  
    1.19  fun domain_type (Type("fun", [T,_])) = T
    1.20  and range_type  (Type("fun", [_,T])) = T;