# HG changeset patch
# User blanchet
# Date 1398639270 -7200
# Node ID ba2fa4e997294be5760ff49341d9ef56b762dfd1
# Parent  644f0d4820a13efd37bbf598247467849f3672bf
more reliable 'name_of_bnf'

diff -r 644f0d4820a1 -r ba2fa4e99729 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 28 00:54:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -609,14 +609,14 @@
 
 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
@@ -1346,10 +1346,10 @@
       | (_, 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);
@@ -1407,8 +1407,7 @@
       [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)]))
diff -r 644f0d4820a1 -r ba2fa4e99729 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 28 00:54:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -2438,7 +2438,8 @@
               (SOME deads) map_b rel_b set_bs consts
             #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
           bs tacss map_bs rel_bs set_bss wit_thmss
-          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
+          ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~
+            all_witss) ~~ map SOME Jrels)
           lthy;
 
         val timer = time (timer "registered new codatatypes as BNFs");
diff -r 644f0d4820a1 -r ba2fa4e99729 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Apr 28 00:54:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -1726,8 +1726,8 @@
               map_b rel_b set_bs consts
             #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
           bs tacss map_bs rel_bs set_bss
-            ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels)
-            lthy;
+            ((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~
+              Iwitss) ~~ map SOME Irels) lthy;
 
         val timer = time (timer "registered new datatypes as BNFs");