src/HOL/BNF/Tools/bnf_lfp.ML

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Sep 12 15:46:44 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Sep 12 16:31:42 2013 +0200
@@ -36,13 +36,17 @@
     val n = length bnfs; (*active*)
     val ks = 1 upto n;
     val m = live - n; (*passive, if 0 don't generate a new BNF*)
+
+    val note_all = Config.get lthy bnf_note_all;
     val b_names = map Binding.name_of bs;
-    val common_name = mk_common_name b_names;
-    val b = Binding.name common_name;
-    val internal_b = Binding.prefix true common_name b;
-    fun qualify_bs internal = map2 (Binding.prefix internal) b_names bs;
-    val internal_bs = qualify_bs true;
-    val external_bs = qualify_bs false;
+    val b_name = mk_common_name b_names;
+    val b = Binding.name b_name;
+    val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
+    fun mk_internal_bs name =
+      map (fn b =>
+        Binding.prefix true b_name (Binding.suffix_name ("_" ^ name) b) |> Binding.conceal) bs;
+    val external_bs = map2 (Binding.prefix false) b_names bs
+      |> note_all = false ? map Binding.conceal;
 
     (* TODO: check if m, n, etc., are sane *)
 
@@ -238,7 +242,7 @@
 
     (* algebra *)
 
-    val alg_bind = Binding.suffix_name ("_" ^ algN) internal_b;
+    val alg_bind = mk_internal_b algN;
     val alg_name = Binding.name_of alg_bind;
     val alg_def_bind = (Thm.def_binding alg_bind, []);
 
@@ -325,7 +329,7 @@
 
     (* morphism *)
 
-    val mor_bind = Binding.suffix_name ("_" ^ morN) internal_b;
+    val mor_bind = mk_internal_b morN;
     val mor_name = Binding.name_of mor_bind;
     val mor_def_bind = (Thm.def_binding mor_bind, []);
 
@@ -712,8 +716,9 @@
 
     val timer = time (timer "min_algs definition & thms");
 
-    fun min_alg_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ min_algN);
-    val min_alg_name = Binding.name_of o min_alg_bind;
+    val min_alg_binds = mk_internal_bs min_algN;
+    fun min_alg_bind i = nth min_alg_binds (i - 1);
+    fun min_alg_name i = Binding.name_of (min_alg_bind i);
     val min_alg_def_bind = rpair [] o Thm.def_binding o min_alg_bind;
 
     fun min_alg_spec i =
@@ -791,7 +796,7 @@
     val timer = time (timer "Minimal algebra definition & thms");
 
     val II_repT = HOLogic.mk_prodT (HOLogic.mk_tupleT II_BTs, HOLogic.mk_tupleT II_sTs);
-    val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
+    val IIT_bind = mk_internal_b IITN;
 
     val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
       typedef (IIT_bind, params, NoSyn)
@@ -824,7 +829,8 @@
     val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
     val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
 
-    fun str_init_bind i = nth internal_bs (i - 1) |> Binding.suffix_name ("_" ^ str_initN);
+    val str_init_binds = mk_internal_bs str_initN;
+    fun str_init_bind i = nth str_init_binds (i - 1);
     val str_init_name = Binding.name_of o str_init_bind;
     val str_init_def_bind = rpair [] o Thm.def_binding o str_init_bind;
 
@@ -953,7 +959,8 @@
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
-      |> fold_map3 (fn b => fn mx => fn car_init => typedef (b, params, mx) car_init NONE
+      |> fold_map3 (fn b => fn mx => fn car_init =>
+        typedef (Binding.conceal b, params, mx) car_init NONE
           (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
             rtac alg_init_thm] 1)) bs mixfixes car_inits
       |>> apsnd split_list o split_list;
@@ -1016,7 +1023,7 @@
 
     fun ctor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctorN);
     val ctor_name = Binding.name_of o ctor_bind;
-    val ctor_def_bind = rpair [] o Thm.def_binding o ctor_bind;
+    val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
 
     fun ctor_spec i abs str map_FT_init x x' =
       let
@@ -1075,7 +1082,7 @@
 
     fun fold_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctor_foldN);
     val fold_name = Binding.name_of o fold_bind;
-    val fold_def_bind = rpair [] o Thm.def_binding o fold_bind;
+    val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
 
     fun fold_spec i T AT =
       let
@@ -1165,7 +1172,7 @@
 
     fun dtor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtorN);
     val dtor_name = Binding.name_of o dtor_bind;
-    val dtor_def_bind = rpair [] o Thm.def_binding o dtor_bind;
+    val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
 
     fun dtor_spec i FT T =
       let
@@ -1238,7 +1245,7 @@
 
     fun rec_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctor_recN);
     val rec_name = Binding.name_of o rec_bind;
-    val rec_def_bind = rpair [] o Thm.def_binding o rec_bind;
+    val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
 
     val rec_strs =
       map3 (fn ctor => fn prod_s => fn mapx =>