src/HOL/Hoare/hoare_tac.ML
changeset 61424 c3658c18b7bc
parent 61125 4c68426800de
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  local
     1.5  
     1.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
     1.7 -fun abs2list (Const (@{const_name uncurry}, _) $ 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, _)) = [Free (x, T)]
    1.10    | abs2list _ = [];
    1.11  
    1.12 @@ -47,7 +47,7 @@
    1.13              Abs (_, T, _) => T
    1.14            | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
    1.15        in
    1.16 -        Const (@{const_name uncurry},
    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;