diff -r 21423597a80d -r b8a53e3a0ee2 src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 28 12:47:55 2010 +0200
@@ -47,11 +47,9 @@
   where "err_semilat L == semilat(Err.sl L)"
 
 
-consts
-  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
-primrec
+primrec strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where
   "strict f Err    = Err"
-  "strict f (OK x) = f x"
+| "strict f (OK x) = f x"
 
 lemma strict_Some [simp]: 
   "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"