1.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Nov 19 14:33:20 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Nov 19 15:05:28 2013 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4      val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
     1.5      fun mk_internal_bs name =
     1.6        map (fn b =>
     1.7 -        Binding.prefix true b_name (Binding.suffix_name ("_" ^ name) b) |> Binding.conceal) bs;
     1.8 +        Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
     1.9      val external_bs = map2 (Binding.prefix false) b_names bs
    1.10        |> note_all = false ? map Binding.conceal;
    1.11  
    1.12 @@ -1695,7 +1695,7 @@
    1.13        ||>> mk_Frees "s" corec_sTs
    1.14        ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
    1.15  
    1.16 -    fun dtor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtorN);
    1.17 +    fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
    1.18      val dtor_name = Binding.name_of o dtor_bind;
    1.19      val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
    1.20  
    1.21 @@ -1747,7 +1747,7 @@
    1.22  
    1.23      val timer = time (timer "dtor definitions & thms");
    1.24  
    1.25 -    fun unfold_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtor_unfoldN);
    1.26 +    fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
    1.27      val unfold_name = Binding.name_of o unfold_bind;
    1.28      val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
    1.29  
    1.30 @@ -1868,7 +1868,7 @@
    1.31        Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
    1.32          map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
    1.33  
    1.34 -    fun ctor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctorN);
    1.35 +    fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
    1.36      val ctor_name = Binding.name_of o ctor_bind;
    1.37      val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
    1.38  
    1.39 @@ -1939,7 +1939,7 @@
    1.40            trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
    1.41        end;
    1.42  
    1.43 -    fun corec_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtor_corecN);
    1.44 +    fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
    1.45      val corec_name = Binding.name_of o corec_bind;
    1.46      val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
    1.47  

     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Nov 19 14:33:20 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Nov 19 15:05:28 2013 +0100
     2.3 @@ -44,7 +44,7 @@
     2.4      val mk_internal_b = Binding.name #> Binding.prefix true b_name #> Binding.conceal;
     2.5      fun mk_internal_bs name =
     2.6        map (fn b =>
     2.7 -        Binding.prefix true b_name (Binding.suffix_name ("_" ^ name) b) |> Binding.conceal) bs;
     2.8 +        Binding.prefix true b_name (Binding.prefix_name (name ^ "_") b) |> Binding.conceal) bs;
     2.9      val external_bs = map2 (Binding.prefix false) b_names bs
    2.10        |> note_all = false ? map Binding.conceal;
    2.11  
    2.12 @@ -1021,7 +1021,7 @@
    2.13      val phis = map2 retype_free (map mk_pred1T Ts) init_phis;
    2.14      val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
    2.15  
    2.16 -    fun ctor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctorN);
    2.17 +    fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
    2.18      val ctor_name = Binding.name_of o ctor_bind;
    2.19      val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
    2.20  
    2.21 @@ -1080,7 +1080,7 @@
    2.22        (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
    2.23      val foldx = HOLogic.choice_const foldT $ fold_fun;
    2.24  
    2.25 -    fun fold_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctor_foldN);
    2.26 +    fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
    2.27      val fold_name = Binding.name_of o fold_bind;
    2.28      val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
    2.29  
    2.30 @@ -1170,7 +1170,7 @@
    2.31        Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
    2.32          map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
    2.33  
    2.34 -    fun dtor_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ dtorN);
    2.35 +    fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
    2.36      val dtor_name = Binding.name_of o dtor_bind;
    2.37      val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
    2.38  
    2.39 @@ -1243,7 +1243,7 @@
    2.40            trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
    2.41        end;
    2.42  
    2.43 -    fun rec_bind i = nth external_bs (i - 1) |> Binding.suffix_name ("_" ^ ctor_recN);
    2.44 +    fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
    2.45      val rec_name = Binding.name_of o rec_bind;
    2.46      val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
    2.47