added dest_binop;
authorwenzelm
Thu Sep 21 19:05:31 2006 +0200 (2006-09-21)
changeset 2067327738ccd0700
parent 20672 b96394d8c702
child 20674 93baed0f741c
added dest_binop;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Sep 21 19:05:22 2006 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Sep 21 19:05:31 2006 +0200
     1.3 @@ -135,6 +135,7 @@
     1.4    val dest_ctyp: ctyp -> ctyp list
     1.5    val dest_comb: cterm -> cterm * cterm
     1.6    val dest_arg: cterm -> cterm
     1.7 +  val dest_binop: cterm -> cterm * cterm
     1.8    val dest_abs: string option -> cterm -> cterm * cterm
     1.9    val adjust_maxidx_cterm: int -> cterm -> cterm
    1.10    val capply: cterm -> cterm -> cterm
    1.11 @@ -272,6 +273,15 @@
    1.12        end
    1.13    | dest_arg _ = raise CTERM "dest_arg";
    1.14  
    1.15 +fun dest_binop (Cterm {t = tm, T = _, thy_ref, maxidx, sorts}) =
    1.16 +  let fun cterm t T = Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} in
    1.17 +    (case tm of
    1.18 +      Const (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
    1.19 +    |  Free (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
    1.20 +    |   Var (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
    1.21 +    | _ => raise CTERM "dest_binop")
    1.22 +  end;
    1.23 +
    1.24  fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
    1.25        let val (y', t') = Term.dest_abs (the_default x a, T, t) in
    1.26          (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},