path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
authorhaftmann
Thu Jul 30 15:20:57 2009 +0200 (2009-07-30)
changeset 323423fabf5b5fc83
parent 32341 c8c17c2e6ceb
child 32343 605877054de7
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
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/hologic.ML	Thu Jul 30 13:52:18 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jul 30 15:20:57 2009 +0200
     1.3 @@ -67,14 +67,18 @@
     1.4    val split_const: typ * typ * typ -> term
     1.5    val mk_split: term -> term
     1.6    val flatten_tupleT: typ -> typ list
     1.7 -  val mk_tupleT: int list list -> typ list -> typ
     1.8 -  val strip_tupleT: int list list -> typ -> typ list
     1.9 +  val mk_tupleT: typ list -> typ
    1.10 +  val strip_tupleT: typ -> typ list
    1.11 +  val mk_tuple: term list -> term
    1.12 +  val strip_tuple: term -> term list
    1.13 +  val mk_ptupleT: int list list -> typ list -> typ
    1.14 +  val strip_ptupleT: int list list -> typ -> typ list
    1.15    val flat_tupleT_paths: typ -> int list list
    1.16 -  val mk_tuple: int list list -> typ -> term list -> term
    1.17 -  val dest_tuple: int list list -> term -> term list
    1.18 +  val mk_ptuple: int list list -> typ -> term list -> term
    1.19 +  val strip_ptuple: int list list -> term -> term list
    1.20    val flat_tuple_paths: term -> int list list
    1.21 -  val mk_splits: int list list -> typ -> typ -> term -> term
    1.22 -  val strip_splits: term -> term * typ list * int list list
    1.23 +  val mk_psplits: int list list -> typ -> typ -> term -> term
    1.24 +  val strip_psplits: term -> term * typ list * int list list
    1.25    val natT: typ
    1.26    val zero: term
    1.27    val is_zero: term -> bool
    1.28 @@ -323,15 +327,33 @@
    1.29  fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    1.30    | flatten_tupleT T = [T];
    1.31  
    1.32 +
    1.33 +(* tuples with right-fold structure *)
    1.34 +
    1.35 +fun mk_tupleT [] = unitT
    1.36 +  | mk_tupleT Ts = foldr1 mk_prodT Ts;
    1.37 +
    1.38 +fun strip_tupleT (Type ("Product_Type.unit", [])) = []
    1.39 +  | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
    1.40 +  | strip_tupleT T = [T];
    1.41 +
    1.42 +fun mk_tuple [] = unit
    1.43 +  | mk_tuple ts = foldr1 mk_prod ts;
    1.44 +
    1.45 +fun strip_tuple (Const ("Product_Type.Unity", _)) = []
    1.46 +  | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
    1.47 +  | strip_tuple t = [t];
    1.48 +
    1.49 +
    1.50  (* tuples with specific arities
    1.51  
    1.52 -  an "arity" of a tuple is a list of lists of integers
    1.53 -  ("factors"), denoting paths to subterms that are pairs
    1.54 +   an "arity" of a tuple is a list of lists of integers,
    1.55 +   denoting paths to subterms that are pairs
    1.56  *)
    1.57  
    1.58 -fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
    1.59 +fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
    1.60  
    1.61 -fun mk_tupleT ps =
    1.62 +fun mk_ptupleT ps =
    1.63    let
    1.64      fun mk p Ts =
    1.65        if p mem ps then
    1.66 @@ -342,12 +364,12 @@
    1.67        else (hd Ts, tl Ts)
    1.68    in fst o mk [] end;
    1.69  
    1.70 -fun strip_tupleT ps =
    1.71 +fun strip_ptupleT ps =
    1.72    let
    1.73      fun factors p T = if p mem ps then (case T of
    1.74          Type ("*", [T1, T2]) =>
    1.75            factors (1::p) T1 @ factors (2::p) T2
    1.76 -      | _ => prod_err "strip_tupleT") else [T]
    1.77 +      | _ => ptuple_err "strip_ptupleT") else [T]
    1.78    in factors [] end;
    1.79  
    1.80  val flat_tupleT_paths =
    1.81 @@ -357,7 +379,7 @@
    1.82        | factors p _ = []
    1.83    in factors [] end;
    1.84  
    1.85 -fun mk_tuple ps =
    1.86 +fun mk_ptuple ps =
    1.87    let
    1.88      fun mk p T ts =
    1.89        if p mem ps then (case T of
    1.90 @@ -366,16 +388,16 @@
    1.91                val (t, ts') = mk (1::p) T1 ts;
    1.92                val (u, ts'') = mk (2::p) T2 ts'
    1.93              in (pair_const T1 T2 $ t $ u, ts'') end
    1.94 -        | _ => prod_err "mk_tuple")
    1.95 +        | _ => ptuple_err "mk_ptuple")
    1.96        else (hd ts, tl ts)
    1.97    in fst oo mk [] end;
    1.98  
    1.99 -fun dest_tuple ps =
   1.100 +fun strip_ptuple ps =
   1.101    let
   1.102      fun dest p t = if p mem ps then (case t of
   1.103          Const ("Pair", _) $ t $ u =>
   1.104            dest (1::p) t @ dest (2::p) u
   1.105 -      | _ => prod_err "dest_tuple") else [t]
   1.106 +      | _ => ptuple_err "strip_ptuple") else [t]
   1.107    in dest [] end;
   1.108  
   1.109  val flat_tuple_paths =
   1.110 @@ -385,24 +407,24 @@
   1.111        | factors p _ = []
   1.112    in factors [] end;
   1.113  
   1.114 -(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
   1.115 +(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
   1.116    with result type T.  The call creates a new term expecting one argument
   1.117    of type S.*)
   1.118 -fun mk_splits ps T T3 u =
   1.119 +fun mk_psplits ps T T3 u =
   1.120    let
   1.121      fun ap ((p, T) :: pTs) =
   1.122            if p mem ps then (case T of
   1.123                Type ("*", [T1, T2]) =>
   1.124                  split_const (T1, T2, map snd pTs ---> T3) $
   1.125                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
   1.126 -            | _ => prod_err "mk_splits")
   1.127 +            | _ => ptuple_err "mk_psplits")
   1.128            else Abs ("x", T, ap pTs)
   1.129        | ap [] =
   1.130            let val k = length ps
   1.131            in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   1.132    in ap [([], T)] end;
   1.133  
   1.134 -val strip_splits =
   1.135 +val strip_psplits =
   1.136    let
   1.137      fun strip [] qs Ts t = (t, Ts, qs)
   1.138        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jul 30 13:52:18 2009 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jul 30 15:20:57 2009 +0200
     2.3 @@ -645,7 +645,7 @@
     2.4  
     2.5  fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
     2.6      (Const ("Collect", _), [u]) =>
     2.7 -      let val (r, Ts, fs) = HOLogic.strip_splits u
     2.8 +      let val (r, Ts, fs) = HOLogic.strip_psplits u
     2.9        in case strip_comb r of
    2.10            (Const (s, T), ts) =>
    2.11              (case (get_clauses thy s, get_assoc_code thy (s, T)) of
     3.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Jul 30 13:52:18 2009 +0200
     3.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Jul 30 15:20:57 2009 +0200
     3.3 @@ -33,10 +33,10 @@
     3.4  val collect_mem_simproc =
     3.5    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     3.6      fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
     3.7 -         let val (u, Ts, ps) = HOLogic.strip_splits t
     3.8 +         let val (u, Ts, ps) = HOLogic.strip_psplits t
     3.9           in case u of
    3.10             (c as Const ("op :", _)) $ q $ S' =>
    3.11 -             (case try (HOLogic.dest_tuple ps) q of
    3.12 +             (case try (HOLogic.strip_ptuple ps) q of
    3.13                  NONE => NONE
    3.14                | SOME ts =>
    3.15                    if not (loose_bvar (S', 0)) andalso
    3.16 @@ -79,7 +79,7 @@
    3.17        fun mk_collect p T t =
    3.18          let val U = HOLogic.dest_setT T
    3.19          in HOLogic.Collect_const U $
    3.20 -          HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    3.21 +          HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    3.22          end;
    3.23        fun decomp (Const (s, _) $ ((m as Const ("op :",
    3.24              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
    3.25 @@ -223,11 +223,11 @@
    3.26    map (fn (x, ps) =>
    3.27      let
    3.28        val U = HOLogic.dest_setT (fastype_of x);
    3.29 -      val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
    3.30 +      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
    3.31      in
    3.32        (cterm_of thy x,
    3.33         cterm_of thy (HOLogic.Collect_const U $
    3.34 -         HOLogic.mk_splits ps U HOLogic.boolT x'))
    3.35 +         HOLogic.mk_psplits ps U HOLogic.boolT x'))
    3.36      end) fs;
    3.37  
    3.38  fun mk_to_pred_eq p fs optfs' T thm =
    3.39 @@ -240,7 +240,7 @@
    3.40        | SOME fs' =>
    3.41            let
    3.42              val (_, U) = split_last (binder_types T);
    3.43 -            val Ts = HOLogic.strip_tupleT fs' U;
    3.44 +            val Ts = HOLogic.strip_ptupleT fs' U;
    3.45              (* FIXME: should cterm_instantiate increment indexes? *)
    3.46              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
    3.47              val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
    3.48 @@ -248,7 +248,7 @@
    3.49            in
    3.50              thm' RS (Drule.cterm_instantiate [(arg_cong_f,
    3.51                cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
    3.52 -                HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
    3.53 +                HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
    3.54                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    3.55            end)
    3.56    in
    3.57 @@ -361,12 +361,12 @@
    3.58      val insts = map (fn (x, ps) =>
    3.59        let
    3.60          val Ts = binder_types (fastype_of x);
    3.61 -        val T = HOLogic.mk_tupleT ps Ts;
    3.62 +        val T = HOLogic.mk_ptupleT ps Ts;
    3.63          val x' = map_type (K (HOLogic.mk_setT T)) x
    3.64        in
    3.65          (cterm_of thy x,
    3.66           cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
    3.67 -           (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
    3.68 +           (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
    3.69        end) fs
    3.70    in
    3.71      thm |>
    3.72 @@ -422,14 +422,14 @@
    3.73          SOME fs =>
    3.74            let
    3.75              val T = HOLogic.dest_setT (fastype_of x);
    3.76 -            val Ts = HOLogic.strip_tupleT fs T;
    3.77 +            val Ts = HOLogic.strip_ptupleT fs T;
    3.78              val x' = map_type (K (Ts ---> HOLogic.boolT)) x
    3.79            in
    3.80              (x, (x',
    3.81                (HOLogic.Collect_const T $
    3.82 -                 HOLogic.mk_splits fs T HOLogic.boolT x',
    3.83 +                 HOLogic.mk_psplits fs T HOLogic.boolT x',
    3.84                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
    3.85 -                 (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
    3.86 +                 (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
    3.87                    x)))))
    3.88            end
    3.89         | NONE => (x, (x, (x, x))))) params;
    3.90 @@ -448,13 +448,13 @@
    3.91             Pretty.str ("of " ^ s ^ " do not agree with types"),
    3.92             Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
    3.93             Pretty.str "of declared parameters"]));
    3.94 -        val Ts = HOLogic.strip_tupleT fs U;
    3.95 +        val Ts = HOLogic.strip_ptupleT fs U;
    3.96          val c' = Free (s ^ "p",
    3.97            map fastype_of params1 @ Ts ---> HOLogic.boolT)
    3.98        in
    3.99          ((c', (fs, U, Ts)),
   3.100           (list_comb (c, params2),
   3.101 -          HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
   3.102 +          HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
   3.103              (list_comb (c', params1))))
   3.104        end) |> split_list |>> split_list;
   3.105      val eqns' = eqns @
   3.106 @@ -484,7 +484,7 @@
   3.107      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   3.108        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
   3.109           fold_rev lambda params (HOLogic.Collect_const U $
   3.110 -           HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
   3.111 +           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
   3.112           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
   3.113  
   3.114      (* prove theorems for converting predicate to set notation *)
   3.115 @@ -495,7 +495,7 @@
   3.116              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.117                (list_comb (p, params3),
   3.118                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   3.119 -                 (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
   3.120 +                 (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   3.121                    list_comb (c, params))))))
   3.122              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   3.123                [def, mem_Collect_eq, split_conv]) 1))
     4.1 --- a/src/HOL/Tools/split_rule.ML	Thu Jul 30 13:52:18 2009 +0200
     4.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Jul 30 15:20:57 2009 +0200
     4.3 @@ -81,7 +81,7 @@
     4.4                let
     4.5                  val Ts = HOLogic.flatten_tupleT T;
     4.6                  val ys = Name.variant_list xs (replicate (length Ts) a);
     4.7 -              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
     4.8 +              in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
     4.9                  (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    4.10                end
    4.11            | mk_tuple _ x = x;
     5.1 --- a/src/HOL/ex/predicate_compile.ML	Thu Jul 30 13:52:18 2009 +0200
     5.2 +++ b/src/HOL/ex/predicate_compile.ML	Thu Jul 30 15:20:57 2009 +0200
     5.3 @@ -68,20 +68,6 @@
     5.4              HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
     5.5    in mk_eqs x xs end;
     5.6  
     5.7 -fun mk_tupleT [] = HOLogic.unitT
     5.8 -  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
     5.9 -
    5.10 -fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
    5.11 -  | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
    5.12 -  | dest_tupleT t = [t]
    5.13 -
    5.14 -fun mk_tuple [] = HOLogic.unit
    5.15 -  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
    5.16 -
    5.17 -fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
    5.18 -  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
    5.19 -  | dest_tuple t = [t]
    5.20 -
    5.21  fun mk_pred_enumT T = Type (@{type_name Predicate.pred}, [T])
    5.22  
    5.23  fun dest_pred_enumT (Type (@{type_name Predicate.pred}, [T])) = T
    5.24 @@ -557,7 +543,7 @@
    5.25    | funT_of T (SOME mode) = let
    5.26       val Ts = binder_types T;
    5.27       val (Us1, Us2) = get_args mode Ts
    5.28 -   in Us1 ---> (mk_pred_enumT (mk_tupleT Us2)) end;
    5.29 +   in Us1 ---> (mk_pred_enumT (HOLogic.mk_tupleT Us2)) end;
    5.30  
    5.31  fun funT'_of (iss, is) T = let
    5.32      val Ts = binder_types T
    5.33 @@ -565,7 +551,7 @@
    5.34      val paramTs' = map2 (fn SOME is => funT'_of ([], is) | NONE => I) iss paramTs 
    5.35      val (inargTs, outargTs) = get_args is argTs
    5.36    in
    5.37 -    (paramTs' @ inargTs) ---> (mk_pred_enumT (mk_tupleT outargTs))
    5.38 +    (paramTs' @ inargTs) ---> (mk_pred_enumT (HOLogic.mk_tupleT outargTs))
    5.39    end; 
    5.40  
    5.41  
    5.42 @@ -593,7 +579,7 @@
    5.43      val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
    5.44      val name = Name.variant names "x";
    5.45      val name' = Name.variant (name :: names) "y";
    5.46 -    val T = mk_tupleT (map fastype_of out_ts);
    5.47 +    val T = HOLogic.mk_tupleT (map fastype_of out_ts);
    5.48      val U = fastype_of success_t;
    5.49      val U' = dest_pred_enumT U;
    5.50      val v = Free (name, T);
    5.51 @@ -601,7 +587,7 @@
    5.52    in
    5.53      lambda v (fst (Datatype.make_case
    5.54        (ProofContext.init thy) false [] v
    5.55 -      [(mk_tuple out_ts,
    5.56 +      [(HOLogic.mk_tuple out_ts,
    5.57          if null eqs'' then success_t
    5.58          else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
    5.59            foldr1 HOLogic.mk_conj eqs'' $ success_t $
    5.60 @@ -609,19 +595,6 @@
    5.61         (v', mk_empty U')]))
    5.62    end;
    5.63  
    5.64 -(*FIXME function can be removed*)
    5.65 -fun mk_funcomp f t =
    5.66 -  let
    5.67 -    val names = Term.add_free_names t [];
    5.68 -    val Ts = binder_types (fastype_of t);
    5.69 -    val vs = map Free
    5.70 -      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
    5.71 -  in
    5.72 -    fold_rev lambda vs (f (list_comb (t, vs)))
    5.73 -  end;
    5.74 -
    5.75 -
    5.76 -
    5.77  fun compile_param_ext thy modes (NONE, t) = t
    5.78    | compile_param_ext thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
    5.79        let
    5.80 @@ -643,11 +616,11 @@
    5.81                  Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
    5.82                else error "compile param: Not an inductive predicate with correct mode"
    5.83            | Free (name, T) => Free (name, funT_of T (SOME is'))
    5.84 -        val outTs = dest_tupleT (dest_pred_enumT (body_type (fastype_of f')))
    5.85 +        val outTs = HOLogic.strip_tupleT (dest_pred_enumT (body_type (fastype_of f')))
    5.86          val out_vs = map Free (out_names ~~ outTs)
    5.87          val params' = map (compile_param thy modes) (ms ~~ params)
    5.88          val f_app = list_comb (f', params' @ inargs)
    5.89 -        val single_t = (mk_single (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
    5.90 +        val single_t = (mk_single (HOLogic.mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
    5.91          val match_t = compile_match thy [] [] out_vs single_t
    5.92        in list_abs (ivs,
    5.93          mk_bind (f_app, match_t))
    5.94 @@ -682,7 +655,7 @@
    5.95                   (curry Library.drop (length ms) (fst (strip_type T)))
    5.96                 val params' = map (compile_param thy modes) (ms ~~ params)
    5.97               in list_comb (Const (predfun_name_of thy name mode, ((map fastype_of params') @ Ts) --->
    5.98 -               mk_pred_enumT (mk_tupleT Us)), params')
    5.99 +               mk_pred_enumT (HOLogic.mk_tupleT Us)), params')
   5.100               end
   5.101             else error "not a valid inductive expression"
   5.102         | (Free (name, T), args) =>
   5.103 @@ -717,7 +690,7 @@
   5.104                out_ts'' (names', map (rpair []) vs);
   5.105            in
   5.106              compile_match thy constr_vs (eqs @ eqs') out_ts'''
   5.107 -              (mk_single (mk_tuple out_ts))
   5.108 +              (mk_single (HOLogic.mk_tuple out_ts))
   5.109            end
   5.110        | compile_prems out_ts vs names ps =
   5.111            let
   5.112 @@ -772,12 +745,12 @@
   5.113      val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
   5.114      val cl_ts =
   5.115        map (fn cl => compile_clause thy
   5.116 -        all_vs param_vs modes mode cl (mk_tuple xs)) cls;
   5.117 +        all_vs param_vs modes mode cl (HOLogic.mk_tuple xs)) cls;
   5.118      val mode_id = predfun_name_of thy s mode
   5.119    in
   5.120      HOLogic.mk_Trueprop (HOLogic.mk_eq
   5.121        (list_comb (Const (mode_id, (Ts1' @ Us1) --->
   5.122 -           mk_pred_enumT (mk_tupleT Us2)),
   5.123 +           mk_pred_enumT (HOLogic.mk_tupleT Us2)),
   5.124           map2 (fn s => fn T => Free (s, T)) param_vs Ts1' @ xs),
   5.125         foldr1 mk_sup cl_ts))
   5.126    end;
   5.127 @@ -808,7 +781,7 @@
   5.128          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   5.129    val args = map Free (argnames ~~ Ts)
   5.130    val (inargs, outargs) = get_args mode args
   5.131 -  val r = mk_Eval (list_comb (x, inargs), mk_tuple outargs)
   5.132 +  val r = mk_Eval (list_comb (x, inargs), HOLogic.mk_tuple outargs)
   5.133    val t = fold_rev lambda args r 
   5.134  in
   5.135    (t, argnames @ names)
   5.136 @@ -834,9 +807,9 @@
   5.137    val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
   5.138    val funargs = params @ inargs
   5.139    val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
   5.140 -                  if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
   5.141 +                  if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
   5.142    val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
   5.143 -                   mk_tuple outargs))
   5.144 +                   HOLogic.mk_tuple outargs))
   5.145    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   5.146    val _ = Output.tracing (Syntax.string_of_term_global thy introtrm) 
   5.147    val simprules = [defthm, @{thm eval_pred},
   5.148 @@ -879,7 +852,7 @@
   5.149             | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
   5.150           in mk_split_lambda' xs t end;
   5.151        val predterm = mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs)))
   5.152 -      val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (mk_tupleT Us2))
   5.153 +      val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (HOLogic.mk_tupleT Us2))
   5.154        val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id)
   5.155        val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
   5.156        val def = Logic.mk_equals (lhs, predterm)
   5.157 @@ -1141,7 +1114,7 @@
   5.158        end
   5.159      else all_tac
   5.160    in
   5.161 -    split_term_tac (mk_tuple out_ts)
   5.162 +    split_term_tac (HOLogic.mk_tuple out_ts)
   5.163      THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
   5.164    end
   5.165  
   5.166 @@ -1536,7 +1509,7 @@
   5.167    let
   5.168      val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
   5.169        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
   5.170 -    val (body, Ts, fp) = HOLogic.strip_splits split;
   5.171 +    val (body, Ts, fp) = HOLogic.strip_psplits split;
   5.172      val (pred as Const (name, T), all_args) = strip_comb body;
   5.173      val (params, args) = chop (nparams_of thy name) all_args;
   5.174      val user_mode = map_filter I (map_index
   5.175 @@ -1556,14 +1529,14 @@
   5.176      val t_eval = if null outargs then t_pred else let
   5.177          val outargs_bounds = map (fn Bound i => i) outargs;
   5.178          val outargsTs = map (nth Ts) outargs_bounds;
   5.179 -        val T_pred = mk_tupleT outargsTs;
   5.180 -        val T_compr = HOLogic.mk_tupleT fp Ts;
   5.181 +        val T_pred = HOLogic.mk_tupleT outargsTs;
   5.182 +        val T_compr = HOLogic.mk_ptupleT fp Ts;
   5.183          val arrange_bounds = map_index I outargs_bounds
   5.184            |> sort (prod_ord (K EQUAL) int_ord)
   5.185            |> map fst;
   5.186          val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
   5.187            (Term.list_abs (map (pair "") outargsTs,
   5.188 -            HOLogic.mk_tuple fp T_compr (map Bound arrange_bounds)))
   5.189 +            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
   5.190        in mk_pred_map T_pred T_compr arrange t_pred end
   5.191    in t_eval end;
   5.192