--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 03 12:48:20 2014 +0100
@@ -190,7 +190,7 @@
fun mk_spec ctr_offset
({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
- {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' recx,
+ {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
in