--- 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"