# HG changeset patch
# User blanchet
# Date 1366967086 -7200
# Node ID 5fe72280a49f2a49642be79e298659ac6dc1a8d1
# Parent  1267c28c7bdd0b85291aacc97b94b614f690ab4c
put an underscore in prefix

diff -r 1267c28c7bdd -r 5fe72280a49f src/HOL/BNF/Examples/Stream.thy
--- 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)
diff -r 1267c28c7bdd -r 5fe72280a49f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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 =