(adjustions)

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

--- a/src/HOL/Lambda/WeakNorm.thy	Mon Nov 06 16:28:36 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Nov 06 16:28:37 2006 +0100
@@ -591,11 +591,11 @@
 structure Type = ROOT.Type;
 structure Lambda = ROOT.Lambda;
 
-fun nat_of_int 0 = ROOT.IntDef.Zero_nat
-  | nat_of_int n = ROOT.IntDef.Succ_nat (nat_of_int (n-1));
+fun nat_of_int 0 = ROOT.Nat.Zero_nat
+  | nat_of_int n = ROOT.Nat.Suc (nat_of_int (n-1));
 
-fun int_of_nat ROOT.IntDef.Zero_nat = 0
-  | int_of_nat (ROOT.IntDef.Succ_nat n) = 1 + int_of_nat n;
+fun int_of_nat ROOT.Nat.Zero_nat = 0
+  | int_of_nat (ROOT.Nat.Suc n) = 1 + int_of_nat n;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
@@ -632,7 +632,7 @@
       let val dBT = dBtype_of_typ T
       in Norm.Abs_1 (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
-        typing_of_term (T :: Ts) (Type.shift e ROOT.IntDef.Zero_nat dBT) t)
+        typing_of_term (T :: Ts) (Type.shift e ROOT.Nat.Zero_nat dBT) t)
       end
   | typing_of_term _ _ _ = error "typing_of_term: bad term";
 

--- a/src/HOL/ex/NormalForm.thy	Mon Nov 06 16:28:36 2006 +0100
+++ b/src/HOL/ex/NormalForm.thy	Mon Nov 06 16:28:37 2006 +0100
@@ -67,8 +67,6 @@
 lemma "[] @ [] = []" by normalization
 lemma "[] @ xs = xs" by normalization
 lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
-lemma "[%a::'x. a, %b. b, c] @ xs = (%x. x) # (%x. x) # c # xs" by normalization
-lemma "[%a::'x. a, %b. b, c] @ [u, v] = [%x. x, %x. x, c, u, v]" by normalization
 lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
 normal_form "map (%f. f True) [id, g, Not] = [True, g True, False]"
 normal_form "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"

--- a/src/Pure/Tools/codegen_funcgr.ML	Mon Nov 06 16:28:36 2006 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML	Mon Nov 06 16:28:37 2006 +0100
@@ -250,7 +250,7 @@
             val ty_decl' = Logic.incr_tvar maxidx ty_decl;
             val maxidx' = Int.max (Term.maxidx_of_typ ty_decl' + 1, maxidx);
           in Type.unify tsig (ty_decl', ty) (env, maxidx')
-          handle TUNIFY => error ("Failed to instantiate\n"
+          handle TUNIFY => setmp show_sorts true error ("Failed to instantiate\n"
             ^ (Sign.string_of_typ thy o Envir.norm_type env) ty_decl' ^ "\nto\n"
             ^ (Sign.string_of_typ thy o Envir.norm_type env) ty ^ ",\n"
             ^ "in function theorems\n"