# HG changeset patch
# User blanchet
# Date 1410177781 -7200
# Node ID cd7868fd8f01adbd485bc03f2464ef0e9d543aab
# Parent  75b3a5e95d68b7020932e28e1262cc7c9ce131c3
tuning

diff -r 75b3a5e95d68 -r cd7868fd8f01 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -526,7 +526,7 @@
     val thy = Proof_Context.theory_of lthy0;
 
     val maybe_conceal_def_binding = Thm.def_binding
-      #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
+      #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
 
     val ((cst, (_, def)), (lthy', lthy)) = lthy0
       |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
@@ -1394,7 +1394,7 @@
             ks xss;
 
         val maybe_conceal_def_binding = Thm.def_binding
-          #> Config.get no_defs_lthy bnf_note_all = false ? Binding.conceal;
+          #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal;
 
         val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
           |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
diff -r 75b3a5e95d68 -r cd7868fd8f01 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -613,7 +613,7 @@
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
     fun pre_qualify b = Binding.qualify false (Binding.name_of b)
-      #> Config.get lthy' bnf_note_all = false ? Binding.conceal;
+      #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
 
     val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
       fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
diff -r 75b3a5e95d68 -r cd7868fd8f01 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -75,7 +75,7 @@
       map (fn b =>
         Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
     val external_bs = map2 (Binding.prefix false) b_names bs
-      |> note_all = false ? map Binding.conceal;
+      |> not note_all ? map Binding.conceal;
 
     (* TODO: check if m, n, etc., are sane *)
 
diff -r 75b3a5e95d68 -r cd7868fd8f01 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -45,7 +45,7 @@
       map (fn b =>
         Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
     val external_bs = map2 (Binding.prefix false) b_names bs
-      |> note_all = false ? map Binding.conceal;
+      |> not note_all ? map Binding.conceal;
 
     (* TODO: check if m, n, etc., are sane *)
 
diff -r 75b3a5e95d68 -r cd7868fd8f01 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -121,15 +121,15 @@
         map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o
           Long_Name.base_name) T_names;
 
-      fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
-        | is_pair_C _ _ = false;
+      fun is_prod_C @{type_name prod} [_, T'] = member (op =) Cs T'
+        | is_prod_C _ _ = false;
 
       fun mk_size_of_typ (T as TFree _) =
           pair (case AList.lookup (op =) As_fs T of
               SOME f => f
             | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
         | mk_size_of_typ (T as Type (s, Ts)) =
-          if is_pair_C s Ts then
+          if is_prod_C s Ts then
             pair (snd_const T)
           else if exists (exists_subtype_in (As @ Cs)) Ts then
             (case Symtab.lookup data s of
@@ -169,7 +169,7 @@
         |>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
 
       val maybe_conceal_def_binding = Thm.def_binding
-        #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
+        #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
 
       val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs [];
       val size_Ts = map fastype_of size_rhss;
diff -r 75b3a5e95d68 -r cd7868fd8f01 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 14:03:01 2014 +0200
@@ -477,12 +477,10 @@
   let
     fun in_single set A =
       let val AT = fastype_of A;
-      in Const (@{const_name less_eq},
-        AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end;
+      in Const (@{const_name less_eq}, AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end;
   in
-    if length sets > 0
-    then HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As))
-    else HOLogic.mk_UNIV T
+    if null sets then HOLogic.mk_UNIV T
+    else HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As))
   end;
 
 fun mk_inj t =