1.1 --- a/src/HOL/BNF/Examples/Stream.thy	Tue Nov 19 15:05:28 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Tue Nov 19 15:43:08 2013 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  code_datatype Stream
     1.5  
     1.6  lemma stream_case_cert:
     1.7 -  assumes "CASE \<equiv> stream_case c"
     1.8 +  assumes "CASE \<equiv> case_stream c"
     1.9    shows "CASE (a ## s) \<equiv> c a s"
    1.10    using assms by simp_all
    1.11  

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 19 15:05:28 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 19 15:43:08 2013 +0100
     2.3 @@ -544,10 +544,10 @@
     2.4  
     2.5      val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters)));
     2.6  
     2.7 -    fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter =
     2.8 +    fun generate_iter pre (f_Tss, _, fss, xssss) ctor_iter =
     2.9        let
    2.10          val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
    2.11 -        val b = mk_binding suf;
    2.12 +        val b = mk_binding pre;
    2.13          val spec =
    2.14            mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
    2.15              mk_iter_body ctor_iter fss xssss);
    2.16 @@ -563,10 +563,10 @@
    2.17  
    2.18      val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
    2.19  
    2.20 -    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
    2.21 +    fun generate_coiter pre ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
    2.22        let
    2.23          val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
    2.24 -        val b = mk_binding suf;
    2.25 +        val b = mk_binding pre;
    2.26          val spec =
    2.27            mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
    2.28              mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter);
    2.29 @@ -1356,7 +1356,7 @@
    2.30                 lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
    2.31              end;
    2.32  
    2.33 -        fun mk_binding suf = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
    2.34 +        fun mk_binding pre = qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
    2.35  
    2.36          fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
    2.37            (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);

     3.1 --- a/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 15:05:28 2013 +0100
     3.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 15:43:08 2013 +0100
     3.3 @@ -390,7 +390,7 @@
     3.4        qualify false
     3.5          (if Binding.is_empty raw_case_binding orelse
     3.6              Binding.eq_name (raw_case_binding, standard_binding) then
     3.7 -           Binding.suffix_name ("_" ^ caseN) fc_b
     3.8 +           Binding.prefix_name (caseN ^ "_") fc_b
     3.9           else
    3.10             raw_case_binding);
    3.11