put an underscore in prefix

--- a/src/HOL/BNF/Examples/Stream.thy	Fri Apr 26 11:04:45 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Fri Apr 26 11:04:46 2013 +0200
@@ -262,15 +262,15 @@
   by (auto simp: cycle_def)
 
 lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []", consumes 0, case_names _ Eqstream])
-  case (Eqstream s1 s2)
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []", consumes 0, case_names _ Eq_stream])
+  case (Eq_stream s1 s2)
   then obtain u where "s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []" by blast
   thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def)
 qed auto
 
 lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])", consumes 0, case_names _ Eqstream])
-  case (Eqstream s1 s2)
+proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])", consumes 0, case_names _ Eq_stream])
+  case (Eq_stream s1 s2)
   then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast
   thus ?case
     by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold)

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 11:04:45 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 11:04:46 2013 +0200
@@ -31,7 +31,7 @@
 open BNF_FP
 open BNF_FP_Def_Sugar_Tactics
 
-val EqN = "Eq";
+val EqN = "Eq_";
 
 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
 fun quasi_unambiguous_case_names names =