src/HOL/ROOT.ML

--- a/src/HOL/ROOT.ML	Tue Sep 24 08:59:24 1996 +0200
+++ b/src/HOL/ROOT.ML	Tue Sep 24 09:02:34 1996 +0200
@@ -38,6 +38,7 @@
 use_thy "RelPow";
 use_thy "Finite";
 use_thy "Sexp";
+use_thy "Option";
 use_thy "List";
 
 init_pps ();