src/HOL/Tools/BNF/bnf_gfp.ML

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jan 07 15:50:09 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jan 07 15:53:39 2016 +0100
@@ -66,7 +66,7 @@
     val m = live - n; (*passive, if 0 don't generate a new BNF*)
     val ls = 1 upto m;
 
-    val note_all = Config.get lthy bnf_note_all;
+    val internals = Config.get lthy bnf_internals;
     val b_names = map Binding.name_of bs;
     val b_name = mk_common_name b_names;
     val b = Binding.name b_name;
@@ -76,7 +76,7 @@
     fun mk_internal_b name = mk_internal_of_b name b;
     fun mk_internal_bs name = map (mk_internal_of_b name) bs;
     val external_bs = map2 (Binding.prefix false) b_names bs
-      |> not note_all ? map Binding.concealed;
+      |> not internals ? map Binding.concealed;
 
     val deads = fold (union (op =)) Dss resDs;
     val names_lthy = fold Variable.declare_typ deads lthy;
@@ -2680,7 +2680,7 @@
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
         bs thmss);
 
-    val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
+    val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
 
     val fp_res =
       {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,