# HG changeset patch
# User traytel
# Date 1347217995 -7200
# Node ID 632f68beff2a5e69a2194ac5e30b196cd3de4b81
# Parent  f9fc2b64c59991544935f8c6c9da08785043f53f
full name of a type as key in bnf table

diff -r f9fc2b64c599 -r 632f68beff2a src/HOL/Codatatype/Basic_BNFs.thy
--- a/src/HOL/Codatatype/Basic_BNFs.thy	Sun Sep 09 19:57:20 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy	Sun Sep 09 21:13:15 2012 +0200
@@ -572,10 +572,6 @@
   qed
 qed auto
 
-bnf_def deadlist = "map id" [] "\<lambda>_::'a list. |lists (UNIV :: 'a set)|" ["[]"]
-by (auto simp add: cinfinite_def wpull_def infinite_UNIV_listI map.id
-  ordLeq_transitive ctwo_def card_of_card_order_on Field_card_of card_of_mono1 ordLeq_cexp2)
-
 (* Finite sets *)
 abbreviation afset where "afset \<equiv> abs_fset"
 abbreviation rfset where "rfset \<equiv> rep_fset"
diff -r f9fc2b64c599 -r 632f68beff2a src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 19:57:20 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 21:13:15 2012 +0200
@@ -726,7 +726,7 @@
   | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
     let
       val tfrees = Term.add_tfreesT T [];
-      val bnf_opt = if null tfrees then NONE else bnf_of lthy (Long_Name.base_name C);
+      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
     in
       (case bnf_opt of
         NONE => ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
@@ -746,9 +746,7 @@
           in ((bnf, deads_lives), (unfold', lthy)) end
         else
           let
-            (* FIXME: we should allow several BNFs with the same base name *)
-            val Tname = Long_Name.base_name C;
-            val name = Binding.name_of b ^ "_" ^ Tname;
+            val name = Binding.name_of b;
             fun qualify i bind =
               let val namei = if i > 0 then name ^ string_of_int i else name;
               in
diff -r f9fc2b64c599 -r 632f68beff2a src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Sun Sep 09 19:57:20 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Sun Sep 09 21:13:15 2012 +0200
@@ -631,7 +631,10 @@
     val dead = length deads;
 
     (*FIXME: check DUP here, not in after_qed*)
-    val key = Name_Space.full_name Name_Space.default_naming b;
+    val key =
+      (case (CA, Binding.eq_name (qualify b, b)) of
+        (Type (C, _), True) => C
+      | _ => Name_Space.full_name Name_Space.default_naming b);
 
     (*TODO: further checks of type of bnf_map*)
     (*TODO: check types of bnf_sets*)
diff -r f9fc2b64c599 -r 632f68beff2a src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:57:20 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 21:13:15 2012 +0200
@@ -166,8 +166,7 @@
       in snd oo add end;
 
     val nested_bnfs =
-      map_filter (bnf_of lthy o Long_Name.base_name)
-        (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
+      map_filter (bnf_of lthy) (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
 
     val timer = time (Timer.startRealTimer ());
 
@@ -456,7 +455,7 @@
 
     fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
       let
-        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
+        val map0 = map_of_bnf (the (bnf_of lthy s));
         val mapx = mk_map Ts Us map0;
         val TUs = map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
         val args = map build_arg TUs;