src/HOL/Tools/BNF/bnf_def.ML

 
 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
 
 val smart_max_inline_term_size = 25; (*FUDGE*)
 
-fun note_bnf_thms fact_policy qualify' bnf_b bnf =
+fun note_bnf_thms fact_policy qualify0 bnf_b bnf =
   let
     val axioms = axioms_of_bnf bnf;
     val facts = facts_of_bnf bnf;
     val wits = wits_of_bnf bnf;
     val qualify =
       let val (_, qs, _) = Binding.dest bnf_b;
-      in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify' end;
+      in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
   in
     (if fact_policy = Note_All then
       let
         val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
         val notes =

         (* arbitrarily use "Fun" as prefix for "fun"*)
         (_, [], @{type_name fun}) => [(Context.theory_name @{theory Fun}, false)]
       | (_, qs, _) => qs)
   in
     thy
-    (*|> Sign.root_path*)
-    (*|> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers*)
+    |> Sign.root_path
+    |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
     |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
-    (*|> Sign.restore_naming thy*)
+    |> Sign.restore_naming thy
   end;
 
 fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f);
 
 fun register_bnf key bnf =

   let
     fun pretty_set sets i = Pretty.block
       [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1,
           Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
 
-    fun pretty_bnf (key, BNF {T = T, map = map, sets = sets, bd = bd,
-      live = live, lives = lives, dead = dead, deads = deads, ...}) =
+    fun pretty_bnf (key, BNF {name, T, map, sets, bd, live, lives, dead, deads, ...}) =
       Pretty.big_list
         (Pretty.string_of (Pretty.block [Pretty.str key, Pretty.str ":", Pretty.brk 1,
           Pretty.quote (Syntax.pretty_typ ctxt T)]))
         ([Pretty.block [Pretty.str "live:", Pretty.brk 1, Pretty.str (string_of_int live),
             Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) lives)],