# HG changeset patch
# User haftmann
# Date 1242065343 -7200
# Node ID ae2b24698695fe1b2e92e21761cc14242daaf0a7
# Parent  ef8210e58ad72ec7b976864edddb0520be16c9a0
fixed merge accident

diff -r ef8210e58ad7 -r ae2b24698695 src/HOL/ex/Predicate_Compile.thy
--- 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
diff -r ef8210e58ad7 -r ae2b24698695 src/HOL/ex/predicate_compile.ML
--- 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