--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 24 18:10:56 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 24 18:10:56 2015 +0100
@@ -2367,7 +2367,7 @@
|> Local_Theory.notes (common_notes @ notes)
(* for "datatype_realizer.ML": *)
|>> name_noted_thms
- (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
+ (fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])