# HG changeset patch
# User blanchet
# Date 1455557237 -3600
# Node ID d2db9719ffb827313e043664001fbb68a3d17a25
# Parent  1abe8175861946520f5e8c7629a960de39126b80
tuning

diff -r 1abe81758619 -r d2db9719ffb8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 15 13:30:04 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 15 18:27:17 2016 +0100
@@ -352,17 +352,15 @@
 structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list);
 
 fun fp_sugars_interpretation name f =
-  FP_Sugar_Plugin.interpretation name
-    (fn fp_sugars => fn lthy =>
-      f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
+  FP_Sugar_Plugin.interpretation name (fn fp_sugars => fn lthy =>
+    f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
 
 val interpret_fp_sugars = FP_Sugar_Plugin.data;
 
-fun register_fp_sugars_raw fp_sugars =
+val register_fp_sugars_raw =
   fold (fn fp_sugar as {T = Type (s, _), ...} =>
-      Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
-    fp_sugars;
+    Local_Theory.declaration {syntax = false, pervasive = true}
+      (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))));
 
 fun register_fp_sugars plugins fp_sugars =
   register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars;
diff -r 1abe81758619 -r d2db9719ffb8 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Feb 15 13:30:04 2016 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Feb 15 18:27:17 2016 +0100
@@ -205,9 +205,8 @@
 structure Ctr_Sugar_Plugin = Plugin(type T = ctr_sugar);
 
 fun ctr_sugar_interpretation name f =
-  Ctr_Sugar_Plugin.interpretation name
-    (fn ctr_sugar => fn lthy =>
-      f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
+  Ctr_Sugar_Plugin.interpretation name (fn ctr_sugar => fn lthy =>
+    f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
 
 val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
 
@@ -228,12 +227,12 @@
       |> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar)
   end;
 
-val isN = "is_";
-val unN = "un_";
-val notN = "not_";
+val is_prefix = "is_";
+val un_prefix = "un_";
+val not_prefix = "not_";
 
-fun mk_unN 1 1 suf = unN ^ suf
-  | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
+fun mk_unN 1 1 suf = un_prefix ^ suf
+  | mk_unN _ l suf = un_prefix ^ suf ^ string_of_int l;
 
 val caseN = "case";
 val case_congN = "case_cong";
@@ -301,11 +300,11 @@
 fun name_of_disc t =
   (case head_of t of
     Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
-    Long_Name.map_base_name (prefix notN) (name_of_disc t')
+    Long_Name.map_base_name (prefix not_prefix) (name_of_disc t')
   | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
-    Long_Name.map_base_name (prefix isN) (name_of_disc t')
+    Long_Name.map_base_name (prefix is_prefix) (name_of_disc t')
   | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
-    Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
+    Long_Name.map_base_name (prefix (not_prefix ^ is_prefix)) (name_of_disc t')
   | t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
 
 val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
@@ -437,7 +436,7 @@
     fun is_disc_binding_valid b =
       not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
 
-    val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr;
+    val standard_disc_binding = Binding.name o prefix is_prefix o base_name_of_ctr;
 
     val disc_bindings =
       raw_disc_bindings