tuning

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 15 11:10:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 15 11:17:44 2014 +0200
@@ -1353,10 +1353,13 @@
     val fpTs = map (domain_type o fastype_of) dtors;
     val fpBTs = map B_ify fpTs;
 
+    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+
     fun massage_simple_notes base =
       filter_out (null o #2)
       #> map (fn (thmN, thms, f_attrs) =>
-        ((Binding.qualify true base (Binding.name thmN), []), map_index (fn (i, thm) => ([thm], f_attrs i)) thms));
+        ((Binding.qualify true base (Binding.name thmN), []),
+         map_index (fn (i, thm) => ([thm], f_attrs i)) thms));
 
     val massage_multi_notes =
       maps (fn (thmN, thmss, attrs) =>
@@ -1365,8 +1368,6 @@
           fp_b_names fpTs thmss)
       #> filter_out (null o fst o hd o snd);
 
-    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
-
     val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
     val ns = map length ctr_Tsss;
     val kss = map (fn n => 1 upto n) ns;

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Sep 15 11:10:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Sep 15 11:17:44 2014 +0200
@@ -77,7 +77,7 @@
   | num_binder_types _ = 0;
 
 val exists_subtype_in = Term.exists_subtype o member (op =);
-fun exists_strict_subtype_in Ts T = exists_subtype_in (filter_out (curry (op =) T) Ts) T;
+fun exists_strict_subtype_in Ts T = exists_subtype_in (remove (op =) T Ts) T;
 
 fun tvar_subst thy Ts Us =
   Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) [];

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 15 11:10:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 15 11:17:44 2014 +0200
@@ -22,13 +22,13 @@
 open BNF_Def
 open BNF_FP_Def_Sugar
 
-val size_plugin = "size"
+val size_plugin = "size";
 
-val size_N = "size_"
+val size_N = "size_";
 
-val rec_o_mapN = "rec_o_map"
-val sizeN = "size"
-val size_o_mapN = "size_o_map"
+val rec_o_mapN = "rec_o_map";
+val sizeN = "size";
+val size_o_mapN = "size_o_map";
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
@@ -50,14 +50,12 @@
 val size_of = Symtab.lookup o Data.get o Context.Proof;
 val size_of_global = Symtab.lookup o Data.get o Context.Theory;
 
-val zero_nat = @{const zero_class.zero (nat)};
-
 fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
 
 fun mk_to_natT T = T --> HOLogic.natT;
 
-fun mk_abs_zero_nat T = Term.absdummy T zero_nat;
+fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero;
 
 fun pointfill ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong);
 
@@ -155,7 +153,7 @@
           val xs = map2 (curry Free) x_names x_Ts;
           val (summands, size_o_maps') =
             fold_map mk_size_of_arg xs size_o_maps
-            |>> remove (op =) zero_nat;
+            |>> remove (op =) HOLogic.zero;
           val sum =
             if null summands then HOLogic.zero
             else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);