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