# HG changeset patch
# User wenzelm
# Date 1324069728 -3600
# Node ID 4e70be32621adf7c3eaa6d3ff8f28011cebab272
# Parent  cea7cd0c7e99528d91c80be03b0c6c281d734cdc
more elementary defs;

diff -r cea7cd0c7e99 -r 4e70be32621a src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 16 21:23:21 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 16 22:08:48 2011 +0100
@@ -233,7 +233,7 @@
         (if length descr' = 1 then [big_reccomb_name]
          else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
     val reccombs =
-      map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+      map (fn ((name, T), T') => Const (name, reccomb_fn_Ts @ [T] ---> T'))
         (reccomb_names ~~ recTs ~~ rec_result_Ts);
 
     val (reccomb_defs, thy2) =
@@ -245,9 +245,9 @@
           (map
             (fn ((((name, comb), set), T), T') =>
               (Binding.name (Long_Name.base_name name ^ "_def"),
-                Logic.mk_equals (comb, absfree ("x", T)
+                Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
                  (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
-                   (set $ Free ("x", T) $ Free ("y", T'))))))
+                   (set $ Free ("x", T) $ Free ("y", T')))))))
             (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
       ||> Sign.parent_path
       ||> Theory.checkpoint;
@@ -325,9 +325,10 @@
             val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
             val def =
               (Binding.name (Long_Name.base_name name ^ "_def"),
-                Logic.mk_equals (list_comb (Const (name, caseT), fns1),
-                  list_comb (reccomb, (flat (take i case_dummy_fns)) @
-                    fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
+                Logic.mk_equals (Const (name, caseT),
+                  fold_rev lambda fns1
+                    (list_comb (reccomb,
+                      flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
             val ([def_thm], thy') =
               thy
               |> Sign.declare_const_global decl |> snd