# HG changeset patch
# User blanchet
# Date 1367317120 -7200
# Node ID 3be0a5c6dc9e9db6a2103cb9c4db6618d550eadf
# Parent  35911d5acfa9ea2bf2027b1ccc137f372b8ae5cd
comment tuning

diff -r 35911d5acfa9 -r 3be0a5c6dc9e src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 12:13:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 12:18:40 2013 +0200
@@ -1283,8 +1283,7 @@
     fun derive_and_note_induct_fold_rec_thms_for_types
         (((ctrss, _, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =
       let
-        val ((induct_thm, induct_thms, induct_attrs),
-             (fold_thmss, fold_attrs),
+        val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
           derive_induct_fold_rec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct fp_fold_thms
             fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As ctrss ctr_defss folds recs fold_defs
@@ -1408,8 +1407,7 @@
 val no_map_rel = (Binding.empty, Binding.empty);
 
 (* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
-   that we don't want them to be highlighted everywhere because of some obscure feature of the BNF
-   package. *)
+   that we don't want them to be highlighted everywhere. *)
 fun extract_map_rel ("map", b) = apfst (K b)
   | extract_map_rel ("rel", b) = apsnd (K b)
   | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);