In Main: moved Bin to the left to preserve the solver in its simpset.

--- a/src/HOL/Arith.ML	Mon Jan 04 16:37:04 1999 +0100
+++ b/src/HOL/Arith.ML	Tue Jan 05 17:27:59 1999 +0100
@@ -849,26 +849,22 @@
 val ccontr = ccontr;
 val conjI = conjI;
 val lessD = Suc_leI;
-val nat_neqE = nat_neqE;
+val neqE = nat_neqE;
 val notI = notI;
 val not_leD = not_leE RS Suc_leI;
 val not_lessD = leI;
 val sym = sym;
 
-val nat = Type("nat",[]);
-val boolT = Type("bool",[]);
-
-fun nnb T = T = ([nat,nat] ---> boolT);
-
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
-  | poly(Const("op +",Type("fun",[Type("nat",[]),_])) $ s $ t, pi) =
-      poly(s,poly(t,pi))
+  | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
   | poly(t,(p,i)) =
-      if t = Const("0",nat) then (p,i)
+      if t = Const("0",HOLogic.natT) then (p,i)
       else (case assoc(p,t) of None => ((t,1)::p,i)
             | Some m => (overwrite(p,(t,m+1)), i))
 
+fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
+
 fun decomp2(rel,T,lhs,rhs) =
   if not(nnb T) then None else
   let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
@@ -908,12 +904,12 @@
 
 fun is_False thm =
   let val _ $ t = #prop(rep_thm thm)
-  in t = Const("False",boolT) end;
+  in t = Const("False",HOLogic.boolT) end;
 
-fun is_nat(t) = fastype_of1 t = nat;
+fun is_nat(t) = fastype_of1 t = HOLogic.natT;
 
 fun mk_nat_thm sg t =
-  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),nat))
+  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   in instantiate ([],[(cn,ct)]) le0 end;
 
 end;

--- a/src/HOL/Main.thy	Mon Jan 04 16:37:04 1999 +0100
+++ b/src/HOL/Main.thy	Tue Jan 05 17:27:59 1999 +0100
@@ -1,4 +1,4 @@
 
 (*theory Main includes everything*)
 
-Main = Map + Recdef + Record + Bin + RelPow + Sexp + String
+Main = Bin + Map + Recdef + Record + RelPow + Sexp + String