src/HOL/Hoare/hoare_tac.ML
changeset 44241 7943b69f0188
parent 42793 88bee9f6eec7
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed Aug 17 16:46:58 2011 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed Aug 17 18:05:31 2011 +0200
     1.3 @@ -28,17 +28,21 @@
     1.4  
     1.5  (** abstraction of body over a tuple formed from a list of free variables.
     1.6  Types are also built **)
     1.7 -fun mk_abstupleC []     body = absfree ("x", HOLogic.unitT, body)
     1.8 -  | mk_abstupleC (v::w) body = let val (n,T) = dest_Free v
     1.9 -                               in if w=[] then absfree (n, T, body)
    1.10 -        else let val z  = mk_abstupleC w body;
    1.11 -                 val T2 = case z of Abs(_,T,_) => T
    1.12 -                        | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    1.13 -       in
    1.14 +fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body
    1.15 +  | mk_abstupleC [v] body = absfree (dest_Free v) body
    1.16 +  | mk_abstupleC (v :: w) body =
    1.17 +      let
    1.18 +        val (x, T) = dest_Free v;
    1.19 +        val z = mk_abstupleC w body;
    1.20 +        val T2 =
    1.21 +          (case z of
    1.22 +            Abs (_, T, _) => T
    1.23 +          | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
    1.24 +      in
    1.25          Const (@{const_name prod_case},
    1.26 -          (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T,T2) --> HOLogic.boolT)
    1.27 -            $ absfree (n, T, z)
    1.28 -       end end;
    1.29 +            (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
    1.30 +          absfree (x, T) z
    1.31 +      end;
    1.32  
    1.33  (** maps [x1,...,xn] to (x1,...,xn) and types**)
    1.34  fun mk_bodyC []      = HOLogic.unit