modernized primrec;

--- a/src/HOL/Extraction/Euclid.thy	Fri Jan 25 23:05:27 2008 +0100
+++ b/src/HOL/Extraction/Euclid.thy	Fri Jan 25 23:50:33 2008 +0100
@@ -128,10 +128,10 @@
 lemma dvd_prod [iff]: "n dvd prod (n # ns)"
   by simp
 
-consts fact :: "nat \<Rightarrow> nat"    ("(_!)" [1000] 999)
-primrec
-  "0! = 1"
-  "(Suc n)! = n! * Suc n"
+primrec fact :: "nat \<Rightarrow> nat"    ("(_!)" [1000] 999)
+where
+    "0! = 1"
+  | "(Suc n)! = n! * Suc n"
 
 lemma fact_greater_0 [iff]: "0 < n!"
   by (induct n) simp_all

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

--- a/src/HOL/Extraction/Warshall.thy	Fri Jan 25 23:05:27 2008 +0100
+++ b/src/HOL/Extraction/Warshall.thy	Fri Jan 25 23:50:33 2008 +0100
@@ -16,22 +16,24 @@
 
 datatype b = T | F
 
-consts
+primrec
   is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+where
+    "is_path' r x [] z = (r x z = T)"
+  | "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)"
 
-primrec
-  "is_path' r x [] z = (r x z = T)"
-  "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)"
-
-constdefs
+definition
   is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow>
     nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-  "is_path r p i j k == fst p = j \<and> snd (snd p) = k \<and>
+where
+  "is_path r p i j k \<longleftrightarrow> fst p = j \<and> snd (snd p) = k \<and>
      list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
      is_path' r (fst p) (fst (snd p)) (snd (snd p))"
 
+definition
   conc :: "('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a)"
-  "conc p q == (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
+where
+  "conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
 
 theorem is_path'_snoc [simp]:
   "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"