--- a/src/HOL/Library/ExecutableSet.thy Wed Mar 21 13:58:36 2007 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Wed Mar 21 16:06:15 2007 +0100
@@ -64,7 +64,7 @@
fun
drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"drop_first f [] = []"
- "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
+| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
declare drop_first.simps [code del]
declare drop_first.simps [code target: List]
@@ -150,7 +150,7 @@
function unions :: "'a list list \<Rightarrow> 'a list"
where
"unions [] = []"
- "unions xs = foldr unionl xs []"
+| "unions xs = foldr unionl xs []"
by pat_completeness auto
termination by lexicographic_order