# HG changeset patch
# User blanchet
# Date 1384872188 -3600
# Node ID 5b34a5b93ec222810879a103940a4f3610361352
# Parent  6fae4ecd4ab396aeed7c9eb65d496c4ac76a4df6
use type suffixes instead of prefixes for 'case', '(un)fold', '(co)rec'

diff -r 6fae4ecd4ab3 -r 5b34a5b93ec2 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Tue Nov 19 15:05:28 2013 +0100
+++ b/src/HOL/BNF/Examples/Stream.thy	Tue Nov 19 15:43:08 2013 +0100
@@ -18,7 +18,7 @@
 code_datatype Stream
 
 lemma stream_case_cert:
-  assumes "CASE \<equiv> stream_case c"
+  assumes "CASE \<equiv> case_stream c"
   shows "CASE (a ## s) \<equiv> c a s"
   using assms by simp_all
 
diff -r 6fae4ecd4ab3 -r 5b34a5b93ec2 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 19 15:05:28 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 19 15:43:08 2013 +0100
@@ -544,10 +544,10 @@
 
     val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters)));
 
-    fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter =
+    fun generate_iter pre (f_Tss, _, fss, xssss) ctor_iter =
       let
         val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
-        val b = mk_binding suf;
+        val b = mk_binding pre;
         val spec =
           mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
             mk_iter_body ctor_iter fss xssss);
@@ -563,10 +563,10 @@
 
     val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
 
-    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
+    fun generate_coiter pre ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
       let
         val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
-        val b = mk_binding suf;
+        val b = mk_binding pre;
         val spec =
           mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
             mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter);
@@ -1356,7 +1356,7 @@
                lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
             end;
 
-        fun mk_binding suf = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
+        fun mk_binding pre = qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
 
         fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
           (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
diff -r 6fae4ecd4ab3 -r 5b34a5b93ec2 src/HOL/Tools/ctr_sugar.ML
--- a/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 15:05:28 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 19 15:43:08 2013 +0100
@@ -390,7 +390,7 @@
       qualify false
         (if Binding.is_empty raw_case_binding orelse
             Binding.eq_name (raw_case_binding, standard_binding) then
-           Binding.suffix_name ("_" ^ caseN) fc_b
+           Binding.prefix_name (caseN ^ "_") fc_b
          else
            raw_case_binding);