--- 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