diff -r d09a58c890e3 -r bcfa6b4b21c6 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 22 08:30:12 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 22 08:30:12 2010 +0100
@@ -119,20 +119,20 @@
     SOME (c, _) => Predicate_Compile_Data.keep_function thy c
   | _ => false
 
-fun mk_prems thy lookup_pred t (names, prems) =
+fun flatten thy lookup_pred t (names, prems) =
   let
-    fun mk_prems' (t as Const (name, T)) (names, prems) =
+    fun flatten' (t as Const (name, T)) (names, prems) =
       (if is_constr thy name orelse (is_none (lookup_pred t)) then
         [(t, (names, prems))]
       else
        (*(if is_none (try lookup_pred t) then
           [(Abs ("uu", fastype_of t, HOLogic.mk_eq (t, Bound 0)), (names, prems))]
         else*) [(the (lookup_pred t), (names, prems))])
-    | mk_prems' (t as Free (f, T)) (names, prems) = 
+    | flatten' (t as Free (f, T)) (names, prems) = 
       (case lookup_pred t of
         SOME t' => [(t', (names, prems))]
       | NONE => [(t, (names, prems))])
-    | mk_prems' (t as Abs _) (names, prems) =
+    | flatten' (t as Abs _) (names, prems) =
       if Predicate_Compile_Aux.is_predT (fastype_of t) then
         ([(Envir.eta_contract t, (names, prems))])
       else
@@ -144,7 +144,7 @@
           val body' = subst_bounds (rev frees, body)
           val resname = Name.variant (absnames @ names) "res"
           val resvar = Free (resname, fastype_of body)
-          val t = mk_prems' body' ([], [])
+          val t = flatten' body' ([], [])
             |> map (fn (res, (inner_names, inner_prems)) =>
               let
                 fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
@@ -163,7 +163,7 @@
         in
           [(t, (names, prems))]
         end
-    | mk_prems' t (names, prems) =
+    | flatten' t (names, prems) =
       if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
         [(t, (names, prems))]
       else
@@ -172,9 +172,9 @@
             (let
               val (_, [B, x, y]) = strip_comb t
             in
-              (mk_prems' x (names, prems)
+              (flatten' x (names, prems)
               |> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B) :: prems))))
-              @ (mk_prems' y (names, prems)
+              @ (flatten' y (names, prems)
               |> map (fn (res, (names, prems)) =>
                 (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B)) :: prems))))
             end)
@@ -182,9 +182,9 @@
             (let
               val (_, [f, g]) = strip_comb t
             in
-              mk_prems' f (names, prems)
+              flatten' f (names, prems)
               |> maps (fn (res, (names, prems)) =>
-                mk_prems' (betapply (g, res)) (names, prems))
+                flatten' (betapply (g, res)) (names, prems))
             end)
         | Const (@{const_name "split"}, _) => 
             (let
@@ -193,7 +193,7 @@
               val (T1, T2) = HOLogic.dest_prodT (fastype_of res)
               val (resv1, resv2) = (Free (res1, T1), Free (res2, T2))
             in
-              mk_prems' (betapplys (g, [resv1, resv2]))
+              flatten' (betapplys (g, [resv1, resv2]))
               (res1 :: res2 :: names,
               HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
             end)
@@ -209,7 +209,7 @@
             val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
             val (_, split_args) = strip_comb split_t
             val match = split_args ~~ args
-            fun mk_prems_of_assm assm =
+            fun flatten_of_assm assm =
               let
                 val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
                 val var_names = Name.variant_list names (map fst vTs)
@@ -219,15 +219,15 @@
                 val (lhss : term list, rhss) =
                   split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems')
               in
-                folds_map mk_prems' lhss (var_names @ names, prems)
+                folds_map flatten' lhss (var_names @ names, prems)
                 |> map (fn (ress, (names, prems)) =>
                   let
                     val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss)
                   in (names, prems' @ prems) end)
-                |> maps (mk_prems' inner_t)
+                |> maps (flatten' inner_t)
               end
           in
-            maps mk_prems_of_assm assms
+            maps flatten_of_assm assms
           end
         else
           let
@@ -246,14 +246,14 @@
             val namesprems =
               case t' of
                 NONE =>
-                  folds_map mk_prems' args (names', prems) |>
+                  folds_map flatten' args (names', prems) |>
                   map
                     (fn (argvs, (names'', prems')) =>
                     let
                       val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
                     in (names'', prem :: prems') end)
               | SOME pred =>
-                  folds_map mk_prems' args (names', prems)
+                  folds_map flatten' args (names', prems)
                   |> map (fn (argvs, (names'', prems')) =>
                     let
                       fun lift_arg T t =
@@ -282,7 +282,7 @@
             map (pair resvar) namesprems
           end
   in
-    mk_prems' (Pattern.eta_long [] t) (names, prems)
+    flatten' (Pattern.eta_long [] t) (names, prems)
   end;
 
 (* assumption: mutual recursive predicates all have the same parameters. *)  
@@ -320,7 +320,7 @@
       else
         let
           val names = Term.add_free_names rhs []
-        in mk_prems thy lookup_pred rhs (names, [])
+        in flatten thy lookup_pred rhs (names, [])
           |> map (fn (resultt, (names', prems)) =>
             Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
         end
@@ -392,7 +392,7 @@
           | NONE => (t, I)
         val (P, args) = (strip_comb lit)
       in
-        folds_map (mk_prems thy lookup_pred) args (names, [])
+        folds_map (flatten thy lookup_pred) args (names, [])
         |> map (fn (resargs, (names', prems')) =>
           let
             val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))