diff -r be6e703908f4 -r 67757f1d5e71 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 09:45:14 2013 +0200
@@ -8,8 +8,21 @@
 signature BNF_FP =
 sig
   type fp_result =
-    BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
-      thm list * thm list * thm list * thm list list * thm list * thm list * thm list
+    {bnfs : BNF_Def.BNF list,
+     dtors : term list,
+     ctors : term list,
+     folds : term list,
+     recs : term list,
+     induct : thm,
+     strong_induct : thm,
+     dtor_ctors : thm list,
+     ctor_dtors : thm list,
+     ctor_injects : thm list,
+     map_thms : thm list,
+     set_thmss : thm list list,
+     rel_thms : thm list,
+     fold_thms : thm list,
+     rec_thms : thm list}
 
   val time: Timer.real_timer -> string -> Timer.real_timer
 
@@ -155,8 +168,21 @@
 open BNF_Util
 
 type fp_result =
-  BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
-    thm list * thm list * thm list * thm list list * thm list * thm list * thm list;
+  {bnfs : BNF_Def.BNF list,
+   dtors : term list,
+   ctors : term list,
+   folds : term list,
+   recs : term list,
+   induct : thm,
+   strong_induct : thm,
+   dtor_ctors : thm list,
+   ctor_dtors : thm list,
+   ctor_injects : thm list,
+   map_thms : thm list,
+   set_thmss : thm list list,
+   rel_thms : thm list,
+   fold_thms : thm list,
+   rec_thms : thm list};
 
 val timing = true;
 fun time timer msg = (if timing