src/HOL/Extraction/Higman.thy

--- a/src/HOL/Extraction/Higman.thy	Mon Nov 06 16:28:36 2006 +0100
+++ b/src/HOL/Extraction/Higman.thy	Mon Nov 06 16:28:37 2006 +0100
@@ -342,7 +342,7 @@
 ML {*
 local
   open ROOT.Higman
-  open ROOT.IntDef
+  open ROOT.Nat
 in
 
 val a = 16807.0;
@@ -361,20 +361,20 @@
   end;
 
 fun f s id_0 = mk_word s 0
-  | f s (Succ_nat n) = f (fst (mk_word s 0)) n;
+  | f s (Suc n) = f (fst (mk_word s 0)) n;
 
 val g1 = snd o (f 20000.0);
 
 val g2 = snd o (f 50000.0);
 
 fun f1 id_0 = [A,A]
-  | f1 (Succ_nat id_0) = [B]
-  | f1 (Succ_nat (Succ_nat id_0)) = [A,B]
+  | f1 (Suc id_0) = [B]
+  | f1 (Suc (Suc id_0)) = [A,B]
   | f1 _ = [];
 
 fun f2 id_0 = [A,A]
-  | f2 (Succ_nat id_0) = [B]
-  | f2 (Succ_nat (Succ_nat id_0)) = [B,A]
+  | f2 (Suc id_0) = [B]
+  | f2 (Suc (Suc id_0)) = [B,A]
   | f2 _ = [];
 
 val xs1 = good_prefix g1;