diff -r bcb1e9b7644b -r 11c6811f232c src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Fri Jan 25 23:05:27 2008 +0100
+++ b/src/HOL/Extraction/Higman.thy	Fri Jan 25 23:50:33 2008 +0100
@@ -234,12 +234,11 @@
   qed
 qed
 
-consts
+primrec
   is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
-
-primrec
-  "is_prefix [] f = True"
-  "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
+where
+    "is_prefix [] f = True"
+  | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
 
 theorem L_idx:
   assumes L: "L w ws"