src/HOL/Hoare/hoare_tac.ML
changeset 55414 eab03e9cee8a
parent 51717 9e7d1c139569
child 55659 4089f6e98ab9
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  local
     1.5  
     1.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
     1.7 -fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     1.8 +fun abs2list (Const (@{const_name case_prod}, _) $ 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 @@ -39,7 +39,7 @@
    1.13              Abs (_, T, _) => T
    1.14            | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
    1.15        in
    1.16 -        Const (@{const_name prod_case},
    1.17 +        Const (@{const_name case_prod},
    1.18              (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
    1.19            absfree (x, T) z
    1.20        end;