diff -r 535fbed859da -r 43545e640877 src/HOL/Library/ExecutableSet.thy
--- 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