--- a/src/HOL/ROOT.ML Thu Jul 08 13:35:33 1999 +0200 +++ b/src/HOL/ROOT.ML Thu Jul 08 13:37:40 1999 +0200 @@ -69,7 +69,7 @@ cd "Integ"; use_thy "IntDef"; use "simproc.ML"; -use_thy "Bin"; +use_thy "IntDiv"; cd ".."; (*the all-in-one theory*)