# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID f704ba9875f69cc1d81a8a82200f37c354425eaf
# Parent  f5422b736c44fd5ec5c836ebdfd519b9328c9a6a
making flat triples to nested tuple to remove general triple functions

diff -r f5422b736c44 -r f704ba9875f6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
@@ -204,12 +204,12 @@
 
 fun rep_pred_data (PredData data) = data;
 
-fun mk_pred_data ((intros, elim), (function_names, predfun_data, needs_random)) =
+fun mk_pred_data ((intros, elim), (function_names, (predfun_data, needs_random))) =
   PredData {intros = intros, elim = elim,
     function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
 
 fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) =
-  mk_pred_data (f ((intros, elim), (function_names, predfun_data, needs_random)))
+  mk_pred_data (f ((intros, elim), (function_names, (predfun_data, needs_random))))
 
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -603,7 +603,7 @@
 
 fun expand_tuples_elim th = th
 
-val no_compilation = ([], [], [])
+val no_compilation = ([], ([], []))
 
 fun fetch_pred_data thy name =
   case try (Inductive.the_inductive (ProofContext.init thy)) name of
@@ -619,9 +619,6 @@
         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index
         val nparams = length (Inductive.params_of (#raw_induct result))
-        (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
-          (expand_tuples_elim pre_elim))*)
-        (* FIXME: missing Inductive Set preprocessing *)
         val ctxt = ProofContext.init thy
         val elim_t = mk_casesrule ctxt pred intros
         val elim =
@@ -633,7 +630,7 @@
 
 fun add_predfun_data name mode data =
   let
-    val add = (apsnd o apsnd3) (cons (mode, mk_predfun_data data))
+    val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate thy name =
@@ -694,14 +691,14 @@
 
 fun defined_function_of compilation pred =
   let
-    val set = (apsnd o apfst3) (cons (compilation, []))
+    val set = (apsnd o apfst) (cons (compilation, []))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
 
 fun set_function_name compilation pred mode name =
   let
-    val set = (apsnd o apfst3)
+    val set = (apsnd o apfst)
       (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
@@ -709,7 +706,7 @@
 
 fun set_needs_random name modes =
   let
-    val set = (apsnd o aptrd3) (K modes)
+    val set = (apsnd o apsnd o apsnd) (K modes)
   in
     PredData.map (Graph.map_node name (map_pred_data set))
   end