fixed merge accident

--- a/src/HOL/ex/Predicate_Compile.thy	Mon May 11 19:54:43 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Mon May 11 20:09:03 2009 +0200
@@ -90,16 +90,14 @@
 
 section {* Example for user interface *}
 
-inductive append ::  "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-where
-  "append [] ys ys"
-| "append xs' ys zs' \<Longrightarrow> append (x#xs') ys (x#zs')"
+inductive append2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+    append2_Nil: "append2 [] xs xs"
+  | append2_Cons: "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
 
-code_pred append
-  using assms by (rule append.cases)
+(*code_pred append2
+  using assms by (rule append2.cases)
 
-thm append_codegen
-thm append_cases
-
+thm append2_codegen
+thm append2_cases*)
 
 end
\ No newline at end of file

--- a/src/HOL/ex/predicate_compile.ML	Mon May 11 19:54:43 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Mon May 11 20:09:03 2009 +0200
@@ -14,7 +14,6 @@
   val strip_intro_concl : term -> int -> (term * (term list * term list))
   val code_ind_intros_attrib : attribute
   val code_ind_cases_attrib : attribute
-  val print_alternative_rules : theory -> theory
   val modename_of: theory -> string -> mode -> string
   val modes_of: theory -> string -> mode list
   val setup : theory -> theory