--- 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