--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:04:26 2012 +0200
@@ -104,7 +104,7 @@
val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
- local_theory -> 'a
+ local_theory -> thm list * 'a
val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
binding list * (string list * string list) -> local_theory -> 'a
@@ -302,13 +302,15 @@
fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
|>> split_list;
+ val pre_map_defs = map map_def_of_bnf bnfs'';
+
val timer = time (timer "Normalization & sealing of BNFs");
val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
val timer = time (timer "FP construction in total");
in
- res
+ (pre_map_defs, res)
end;
fun fp_bnf construct bs mixfixes resBs eqs lthy =
@@ -333,7 +335,7 @@
(bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
bs raw_bnfs (empty_unfold, lthy));
in
- mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy'
+ snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')
end;
end;