# HG changeset patch
# User bulwahn
# Date 1269243012 -3600
# Node ID d09a58c890e3611a9f77e4f1da677e59c7f258f4
# Parent  28e73b3e7b6cc70675b4cd57467be4ee2aa93d82
simplifying function flattening

diff -r 28e73b3e7b6c -r d09a58c890e3 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 22 00:51:18 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 22 08:30:12 2010 +0100
@@ -239,24 +239,20 @@
             val resvar = Free (resname, body_type (fastype_of t))
             val _ = assert (fastype_of t = body_type (fastype_of t))
             val names' = resname :: names
-            fun mk_prems'' (t as Const (c, _)) =
-              if is_constr thy c orelse (is_none (lookup_pred t)) then
-                let
-                  val _ = ()(*tracing ("not translating function " ^ Syntax.string_of_term_global thy t)*)
-                in
-                folds_map mk_prems' 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)
-                end
-              else
-                let
-                  (* lookup_pred is falsch für polymorphe Argumente und bool. *)
-                  val pred = the (lookup_pred t)
-                  val Ts = binder_types (fastype_of pred)
-                in
+            val t' = lookup_pred f
+            val Ts = case t' of
+              SOME pred => (fst (split_last (binder_types (fastype_of pred))))
+            | NONE => binder_types (fastype_of t)
+            val namesprems =
+              case t' of
+                NONE =>
+                  folds_map mk_prems' 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)
                   |> map (fn (argvs, (names'', prems')) =>
                     let
@@ -279,24 +275,11 @@
                           end
                       (*val _ = tracing ("Ts: " ^ commas (map (Syntax.string_of_typ_global thy) Ts))
                       val _ = map2 check_arity Ts (map fastype_of (argvs @ [resvar]))*)
-                      val argvs' = map2 lift_arg (fst (split_last Ts)) argvs
+                      val argvs' = map2 lift_arg Ts argvs
                       val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
                     in (names'', prem :: prems') end)
-                end
-            | mk_prems'' (t as Free (_, _)) =
-              folds_map mk_prems' args (names', prems) |>
-                map
-                  (fn (argvs, (names'', prems')) =>
-                  let
-                    val prem = 
-                      case lookup_pred t of
-                        NONE => HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
-                      | SOME p => HOLogic.mk_Trueprop (list_comb (p, argvs @ [resvar]))
-                  in (names'', prem :: prems') end)
-            | mk_prems'' t =
-              error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
           in
-            map (pair resvar) (mk_prems'' f)
+            map (pair resvar) namesprems
           end
   in
     mk_prems' (Pattern.eta_long [] t) (names, prems)