src/HOL/Hoare/hoare_tac.ML
changeset 37591 d3daea901123
parent 37391 476270a6c2dc
child 37677 c5a8b612e571
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  local open HOLogic in
     1.5  
     1.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
     1.7 -fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     1.8 +fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     1.9    | abs2list (Abs (x, T, t)) = [Free (x, T)]
    1.10    | abs2list _ = [];
    1.11  
    1.12 @@ -32,7 +32,7 @@
    1.13          else let val z  = mk_abstupleC w body;
    1.14                   val T2 = case z of Abs(_,T,_) => T
    1.15                          | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    1.16 -       in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    1.17 +       in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    1.18            $ absfree (n, T, z) end end;
    1.19  
    1.20  (** maps [x1,...,xn] to (x1,...,xn) and types**)