src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 55464 56fa33537869
parent 55067 a452de24a877
child 55480 59cc4a8bc28a
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Feb 14 07:53:45 2014 +0100
     1.3 @@ -569,8 +569,9 @@
     1.4            val (bs, attrss) = map_split (fst o nth specs) poss;
     1.5            val notes =
     1.6              map3 (fn b => fn attrs => fn thm =>
     1.7 -              ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), [([thm], [])]))
     1.8 -            bs attrss thms;
     1.9 +                ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs),
    1.10 +                 [([thm], [])]))
    1.11 +              bs attrss thms;
    1.12          in
    1.13            ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
    1.14          end);