src/HOL/Codatatype/Tools/bnf_comp.ML
changeset 49236 632f68beff2a
parent 49228 e43910ccee74
child 49303 c87930fb5b90
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 19:57:20 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 21:13:15 2012 +0200
     1.3 @@ -726,7 +726,7 @@
     1.4    | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
     1.5      let
     1.6        val tfrees = Term.add_tfreesT T [];
     1.7 -      val bnf_opt = if null tfrees then NONE else bnf_of lthy (Long_Name.base_name C);
     1.8 +      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
     1.9      in
    1.10        (case bnf_opt of
    1.11          NONE => ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
    1.12 @@ -746,9 +746,7 @@
    1.13            in ((bnf, deads_lives), (unfold', lthy)) end
    1.14          else
    1.15            let
    1.16 -            (* FIXME: we should allow several BNFs with the same base name *)
    1.17 -            val Tname = Long_Name.base_name C;
    1.18 -            val name = Binding.name_of b ^ "_" ^ Tname;
    1.19 +            val name = Binding.name_of b;
    1.20              fun qualify i bind =
    1.21                let val namei = if i > 0 then name ^ string_of_int i else name;
    1.22                in