diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/PreList.thy	Mon May 08 20:59:30 2000 +0200
@@ -8,8 +8,7 @@
 *)
 
 theory PreList =
-  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
-  + SVC_Oracle
+  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
 files "Integ/NatSimprocs.ML":
 
 end