cleaned up abstract tuple operations and named them consistently
authorhaftmann
Wed Jul 29 16:48:34 2009 +0200 (2009-07-29)
changeset 3228765d5c5b30747
parent 32274 e7f275d203bc
child 32288 168f31155c5e
cleaned up abstract tuple operations and named them consistently
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/split_rule.ML
src/HOL/ex/predicate_compile.ML
     1.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed Jul 29 16:43:02 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Jul 29 16:48:34 2009 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  val alpha  = mk_vartype "'a"
     1.5  val beta   = mk_vartype "'b"
     1.6  
     1.7 -val strip_prod_type = HOLogic.prodT_factors;
     1.8 +val strip_prod_type = HOLogic.flatten_tupleT;
     1.9  
    1.10  
    1.11  
     2.1 --- a/src/HOL/Tools/hologic.ML	Wed Jul 29 16:43:02 2009 +0200
     2.2 +++ b/src/HOL/Tools/hologic.ML	Wed Jul 29 16:48:34 2009 +0200
     2.3 @@ -66,17 +66,15 @@
     2.4    val mk_snd: term -> term
     2.5    val split_const: typ * typ * typ -> term
     2.6    val mk_split: term -> term
     2.7 -  val prodT_factors: typ -> typ list
     2.8 -  val mk_tuple: typ -> term list -> term
     2.9 -  val dest_tuple: term -> term list
    2.10 -  val ap_split: typ -> typ -> term -> term
    2.11 -  val prod_factors: term -> int list list
    2.12 -  val dest_tuple': int list list -> term -> term list
    2.13 -  val prodT_factors': int list list -> typ -> typ list
    2.14 -  val ap_split': int list list -> typ -> typ -> term -> term
    2.15 -  val mk_tuple': int list list -> typ -> term list -> term
    2.16 +  val flatten_tupleT: typ -> typ list
    2.17    val mk_tupleT: int list list -> typ list -> typ
    2.18 -  val strip_split: term -> term * typ list * int list list
    2.19 +  val strip_tupleT: int list list -> typ -> typ list
    2.20 +  val flat_tupleT_paths: typ -> int list list
    2.21 +  val mk_tuple: int list list -> typ -> term list -> term
    2.22 +  val dest_tuple: int list list -> term -> term list
    2.23 +  val flat_tuple_paths: term -> int list list
    2.24 +  val mk_splits: int list list -> typ -> typ -> term -> term
    2.25 +  val strip_splits: term -> term * typ list * int list list
    2.26    val natT: typ
    2.27    val zero: term
    2.28    val is_zero: term -> bool
    2.29 @@ -320,95 +318,17 @@
    2.30    | _ => raise TERM ("mk_split: bad body type", [t]));
    2.31  
    2.32  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
    2.33 -fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
    2.34 -  | prodT_factors T = [T];
    2.35 -
    2.36 -(*Makes a nested tuple from a list, following the product type structure*)
    2.37 -fun mk_tuple (Type ("*", [T1, T2])) tms =
    2.38 -        mk_prod (mk_tuple T1 tms,
    2.39 -                 mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
    2.40 -  | mk_tuple T (t::_) = t;
    2.41 -
    2.42 -fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
    2.43 -  | dest_tuple t = [t];
    2.44 +fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    2.45 +  | flatten_tupleT T = [T];
    2.46  
    2.47 -(*In ap_split S T u, term u expects separate arguments for the factors of S,
    2.48 -  with result type T.  The call creates a new term expecting one argument
    2.49 -  of type S.*)
    2.50 -fun ap_split T T3 u =
    2.51 -  let
    2.52 -    fun ap (T :: Ts) =
    2.53 -          (case T of
    2.54 -             Type ("*", [T1, T2]) =>
    2.55 -               split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
    2.56 -           | _ => Abs ("x", T, ap Ts))
    2.57 -      | ap [] =
    2.58 -          let val k = length (prodT_factors T)
    2.59 -          in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
    2.60 -  in ap [T] end;
    2.61 +(* tuples with specific arities
    2.62  
    2.63 -
    2.64 -(* operations on tuples with specific arities *)
    2.65 -(*
    2.66    an "arity" of a tuple is a list of lists of integers
    2.67    ("factors"), denoting paths to subterms that are pairs
    2.68  *)
    2.69  
    2.70  fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
    2.71  
    2.72 -fun prod_factors t =
    2.73 -  let
    2.74 -    fun factors p (Const ("Pair", _) $ t $ u) =
    2.75 -          p :: factors (1::p) t @ factors (2::p) u
    2.76 -      | factors p _ = []
    2.77 -  in factors [] t end;
    2.78 -
    2.79 -fun dest_tuple' ps =
    2.80 -  let
    2.81 -    fun dest p t = if p mem ps then (case t of
    2.82 -        Const ("Pair", _) $ t $ u =>
    2.83 -          dest (1::p) t @ dest (2::p) u
    2.84 -      | _ => prod_err "dest_tuple'") else [t]
    2.85 -  in dest [] end;
    2.86 -
    2.87 -fun prodT_factors' ps =
    2.88 -  let
    2.89 -    fun factors p T = if p mem ps then (case T of
    2.90 -        Type ("*", [T1, T2]) =>
    2.91 -          factors (1::p) T1 @ factors (2::p) T2
    2.92 -      | _ => prod_err "prodT_factors'") else [T]
    2.93 -  in factors [] end;
    2.94 -
    2.95 -(*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
    2.96 -  with result type T.  The call creates a new term expecting one argument
    2.97 -  of type S.*)
    2.98 -fun ap_split' ps T T3 u =
    2.99 -  let
   2.100 -    fun ap ((p, T) :: pTs) =
   2.101 -          if p mem ps then (case T of
   2.102 -              Type ("*", [T1, T2]) =>
   2.103 -                split_const (T1, T2, map snd pTs ---> T3) $
   2.104 -                  ap ((1::p, T1) :: (2::p, T2) :: pTs)
   2.105 -            | _ => prod_err "ap_split'")
   2.106 -          else Abs ("x", T, ap pTs)
   2.107 -      | ap [] =
   2.108 -          let val k = length ps
   2.109 -          in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   2.110 -  in ap [([], T)] end;
   2.111 -
   2.112 -fun mk_tuple' ps =
   2.113 -  let
   2.114 -    fun mk p T ts =
   2.115 -      if p mem ps then (case T of
   2.116 -          Type ("*", [T1, T2]) =>
   2.117 -            let
   2.118 -              val (t, ts') = mk (1::p) T1 ts;
   2.119 -              val (u, ts'') = mk (2::p) T2 ts'
   2.120 -            in (pair_const T1 T2 $ t $ u, ts'') end
   2.121 -        | _ => prod_err "mk_tuple'")
   2.122 -      else (hd ts, tl ts)
   2.123 -  in fst oo mk [] end;
   2.124 -
   2.125  fun mk_tupleT ps =
   2.126    let
   2.127      fun mk p Ts =
   2.128 @@ -420,7 +340,67 @@
   2.129        else (hd Ts, tl Ts)
   2.130    in fst o mk [] end;
   2.131  
   2.132 -fun strip_split t =
   2.133 +fun strip_tupleT ps =
   2.134 +  let
   2.135 +    fun factors p T = if p mem ps then (case T of
   2.136 +        Type ("*", [T1, T2]) =>
   2.137 +          factors (1::p) T1 @ factors (2::p) T2
   2.138 +      | _ => prod_err "strip_tupleT") else [T]
   2.139 +  in factors [] end;
   2.140 +
   2.141 +val flat_tupleT_paths =
   2.142 +  let
   2.143 +    fun factors p (Type ("*", [T1, T2])) =
   2.144 +          p :: factors (1::p) T1 @ factors (2::p) T2
   2.145 +      | factors p _ = []
   2.146 +  in factors [] end;
   2.147 +
   2.148 +fun mk_tuple ps =
   2.149 +  let
   2.150 +    fun mk p T ts =
   2.151 +      if p mem ps then (case T of
   2.152 +          Type ("*", [T1, T2]) =>
   2.153 +            let
   2.154 +              val (t, ts') = mk (1::p) T1 ts;
   2.155 +              val (u, ts'') = mk (2::p) T2 ts'
   2.156 +            in (pair_const T1 T2 $ t $ u, ts'') end
   2.157 +        | _ => prod_err "mk_tuple")
   2.158 +      else (hd ts, tl ts)
   2.159 +  in fst oo mk [] end;
   2.160 +
   2.161 +fun dest_tuple ps =
   2.162 +  let
   2.163 +    fun dest p t = if p mem ps then (case t of
   2.164 +        Const ("Pair", _) $ t $ u =>
   2.165 +          dest (1::p) t @ dest (2::p) u
   2.166 +      | _ => prod_err "dest_tuple") else [t]
   2.167 +  in dest [] end;
   2.168 +
   2.169 +val flat_tuple_paths =
   2.170 +  let
   2.171 +    fun factors p (Const ("Pair", _) $ t $ u) =
   2.172 +          p :: factors (1::p) t @ factors (2::p) u
   2.173 +      | factors p _ = []
   2.174 +  in factors [] end;
   2.175 +
   2.176 +(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
   2.177 +  with result type T.  The call creates a new term expecting one argument
   2.178 +  of type S.*)
   2.179 +fun mk_splits ps T T3 u =
   2.180 +  let
   2.181 +    fun ap ((p, T) :: pTs) =
   2.182 +          if p mem ps then (case T of
   2.183 +              Type ("*", [T1, T2]) =>
   2.184 +                split_const (T1, T2, map snd pTs ---> T3) $
   2.185 +                  ap ((1::p, T1) :: (2::p, T2) :: pTs)
   2.186 +            | _ => prod_err "mk_splits")
   2.187 +          else Abs ("x", T, ap pTs)
   2.188 +      | ap [] =
   2.189 +          let val k = length ps
   2.190 +          in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   2.191 +  in ap [([], T)] end;
   2.192 +
   2.193 +val strip_splits =
   2.194    let
   2.195      fun strip [] qs Ts t = (t, Ts, qs)
   2.196        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   2.197 @@ -429,7 +409,7 @@
   2.198        | strip (p :: ps) qs Ts t = strip ps qs
   2.199            (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
   2.200            (incr_boundvars 1 t $ Bound 0)
   2.201 -  in strip [[]] [] [] t end;
   2.202 +  in strip [[]] [] [] end;
   2.203  
   2.204  
   2.205  (* nat *)
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Jul 29 16:43:02 2009 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Jul 29 16:48:34 2009 +0200
     3.3 @@ -645,7 +645,7 @@
     3.4  
     3.5  fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
     3.6      (Const ("Collect", _), [u]) =>
     3.7 -      let val (r, Ts, fs) = HOLogic.strip_split u
     3.8 +      let val (r, Ts, fs) = HOLogic.strip_splits u
     3.9        in case strip_comb r of
    3.10            (Const (s, T), ts) =>
    3.11              (case (get_clauses thy s, get_assoc_code thy (s, T)) of
     4.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jul 29 16:43:02 2009 +0200
     4.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jul 29 16:48:34 2009 +0200
     4.3 @@ -33,10 +33,10 @@
     4.4  val collect_mem_simproc =
     4.5    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     4.6      fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
     4.7 -         let val (u, Ts, ps) = HOLogic.strip_split t
     4.8 +         let val (u, Ts, ps) = HOLogic.strip_splits t
     4.9           in case u of
    4.10             (c as Const ("op :", _)) $ q $ S' =>
    4.11 -             (case try (HOLogic.dest_tuple' ps) q of
    4.12 +             (case try (HOLogic.dest_tuple ps) q of
    4.13                  NONE => NONE
    4.14                | SOME ts =>
    4.15                    if not (loose_bvar (S', 0)) andalso
    4.16 @@ -79,7 +79,7 @@
    4.17        fun mk_collect p T t =
    4.18          let val U = HOLogic.dest_setT T
    4.19          in HOLogic.Collect_const U $
    4.20 -          HOLogic.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t
    4.21 +          HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    4.22          end;
    4.23        fun decomp (Const (s, _) $ ((m as Const ("op :",
    4.24              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
    4.25 @@ -223,11 +223,11 @@
    4.26    map (fn (x, ps) =>
    4.27      let
    4.28        val U = HOLogic.dest_setT (fastype_of x);
    4.29 -      val x' = map_type (K (HOLogic.prodT_factors' ps U ---> HOLogic.boolT)) x
    4.30 +      val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
    4.31      in
    4.32        (cterm_of thy x,
    4.33         cterm_of thy (HOLogic.Collect_const U $
    4.34 -         HOLogic.ap_split' ps U HOLogic.boolT x'))
    4.35 +         HOLogic.mk_splits ps U HOLogic.boolT x'))
    4.36      end) fs;
    4.37  
    4.38  fun mk_to_pred_eq p fs optfs' T thm =
    4.39 @@ -240,7 +240,7 @@
    4.40        | SOME fs' =>
    4.41            let
    4.42              val (_, U) = split_last (binder_types T);
    4.43 -            val Ts = HOLogic.prodT_factors' fs' U;
    4.44 +            val Ts = HOLogic.strip_tupleT fs' U;
    4.45              (* FIXME: should cterm_instantiate increment indexes? *)
    4.46              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
    4.47              val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
    4.48 @@ -248,7 +248,7 @@
    4.49            in
    4.50              thm' RS (Drule.cterm_instantiate [(arg_cong_f,
    4.51                cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
    4.52 -                HOLogic.Collect_const U $ HOLogic.ap_split' fs' U
    4.53 +                HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
    4.54                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    4.55            end)
    4.56    in
    4.57 @@ -270,7 +270,7 @@
    4.58               fun factors_of t fs = case strip_abs_body t of
    4.59                   Const ("op :", _) $ u $ S =>
    4.60                     if is_Free S orelse is_Var S then
    4.61 -                     let val ps = HOLogic.prod_factors u
    4.62 +                     let val ps = HOLogic.flat_tuple_paths u
    4.63                       in (SOME ps, (S, ps) :: fs) end
    4.64                     else (NONE, fs)
    4.65                 | _ => (NONE, fs);
    4.66 @@ -279,7 +279,7 @@
    4.67               val ((h', ts'), fs') = (case rhs of
    4.68                   Abs _ => (case strip_abs_body rhs of
    4.69                       Const ("op :", _) $ u $ S =>
    4.70 -                       (strip_comb S, SOME (HOLogic.prod_factors u))
    4.71 +                       (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
    4.72                     | _ => error "member symbol on right-hand side expected")
    4.73                 | _ => (strip_comb rhs, NONE))
    4.74             in
    4.75 @@ -366,7 +366,7 @@
    4.76        in
    4.77          (cterm_of thy x,
    4.78           cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
    4.79 -           (HOLogic.mk_tuple' ps T (map Bound (length ps downto 0)), x'))))
    4.80 +           (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
    4.81        end) fs
    4.82    in
    4.83      thm |>
    4.84 @@ -412,7 +412,7 @@
    4.85        PredSetConvData.get (Context.Proof ctxt);
    4.86      fun infer (Abs (_, _, t)) = infer t
    4.87        | infer (Const ("op :", _) $ t $ u) =
    4.88 -          infer_arities thy set_arities (SOME (HOLogic.prod_factors t), u)
    4.89 +          infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
    4.90        | infer (t $ u) = infer t #> infer u
    4.91        | infer _ = I;
    4.92      val new_arities = filter_out
    4.93 @@ -422,14 +422,14 @@
    4.94          SOME fs =>
    4.95            let
    4.96              val T = HOLogic.dest_setT (fastype_of x);
    4.97 -            val Ts = HOLogic.prodT_factors' fs T;
    4.98 +            val Ts = HOLogic.strip_tupleT fs T;
    4.99              val x' = map_type (K (Ts ---> HOLogic.boolT)) x
   4.100            in
   4.101              (x, (x',
   4.102                (HOLogic.Collect_const T $
   4.103 -                 HOLogic.ap_split' fs T HOLogic.boolT x',
   4.104 +                 HOLogic.mk_splits fs T HOLogic.boolT x',
   4.105                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   4.106 -                 (HOLogic.mk_tuple' fs T (map Bound (length fs downto 0)),
   4.107 +                 (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
   4.108                    x)))))
   4.109            end
   4.110         | NONE => (x, (x, (x, x))))) params;
   4.111 @@ -448,13 +448,13 @@
   4.112             Pretty.str ("of " ^ s ^ " do not agree with types"),
   4.113             Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
   4.114             Pretty.str "of declared parameters"]));
   4.115 -        val Ts = HOLogic.prodT_factors' fs U;
   4.116 +        val Ts = HOLogic.strip_tupleT fs U;
   4.117          val c' = Free (s ^ "p",
   4.118            map fastype_of params1 @ Ts ---> HOLogic.boolT)
   4.119        in
   4.120          ((c', (fs, U, Ts)),
   4.121           (list_comb (c, params2),
   4.122 -          HOLogic.Collect_const U $ HOLogic.ap_split' fs U HOLogic.boolT
   4.123 +          HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
   4.124              (list_comb (c', params1))))
   4.125        end) |> split_list |>> split_list;
   4.126      val eqns' = eqns @
   4.127 @@ -484,7 +484,7 @@
   4.128      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   4.129        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
   4.130           fold_rev lambda params (HOLogic.Collect_const U $
   4.131 -           HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
   4.132 +           HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
   4.133           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
   4.134  
   4.135      (* prove theorems for converting predicate to set notation *)
   4.136 @@ -495,7 +495,7 @@
   4.137              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   4.138                (list_comb (p, params3),
   4.139                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   4.140 -                 (HOLogic.mk_tuple' fs U (map Bound (length fs downto 0)),
   4.141 +                 (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
   4.142                    list_comb (c, params))))))
   4.143              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   4.144                [def, mem_Collect_eq, split_conv]) 1))
     5.1 --- a/src/HOL/Tools/split_rule.ML	Wed Jul 29 16:43:02 2009 +0200
     5.2 +++ b/src/HOL/Tools/split_rule.ML	Wed Jul 29 16:48:34 2009 +0200
     5.3 @@ -50,13 +50,13 @@
     5.4        internal_split_const (T1, T2, T3) $
     5.5        Abs ("v", T1,
     5.6            ap_split T2 T3
     5.7 -             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
     5.8 +             ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
     5.9                Bound 0))
    5.10    | ap_split T T3 u = u;
    5.11  
    5.12  (*Curries any Var of function type in the rule*)
    5.13  fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
    5.14 -      let val T' = HOLogic.prodT_factors T1 ---> T2;
    5.15 +      let val T' = HOLogic.flatten_tupleT T1 ---> T2;
    5.16            val newt = ap_split T1 T2 (Var (v, T'));
    5.17            val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    5.18        in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    5.19 @@ -66,7 +66,7 @@
    5.20  (* complete splitting of partially splitted rules *)
    5.21  
    5.22  fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    5.23 -      (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
    5.24 +      (ap_split T (List.concat (map HOLogic.flatten_tupleT Ts) ---> U)
    5.25          (incr_boundvars 1 u) $ Bound 0))
    5.26    | ap_split' _ _ u = u;
    5.27  
    5.28 @@ -76,10 +76,10 @@
    5.29          val (Us', U') = strip_type T;
    5.30          val Us = Library.take (length ts, Us');
    5.31          val U = Library.drop (length ts, Us') ---> U';
    5.32 -        val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
    5.33 +        val T' = List.concat (map HOLogic.flatten_tupleT Us) ---> U;
    5.34          fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    5.35                let
    5.36 -                val Ts = HOLogic.prodT_factors T;
    5.37 +                val Ts = HOLogic.flatten_tupleT T;
    5.38                  val ys = Name.variant_list xs (replicate (length Ts) a);
    5.39                in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    5.40                  (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
     6.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Jul 29 16:43:02 2009 +0200
     6.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Jul 29 16:48:34 2009 +0200
     6.3 @@ -1531,7 +1531,7 @@
     6.4    let
     6.5      val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
     6.6        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
     6.7 -    val (body, Ts, fp) = HOLogic.strip_split split;
     6.8 +    val (body, Ts, fp) = HOLogic.strip_splits split;
     6.9        (*FIXME former order of tuple positions must be restored*)
    6.10      val (pred as Const (name, T), all_args) = strip_comb body
    6.11      val (params, args) = chop (nparams_of thy name) all_args