src/HOL/ROOT.ML
changeset 21909 a6439243512b
parent 21246 e0e555b67fe5
child 22946 9793d28d49ad
--- a/src/HOL/ROOT.ML	Wed Dec 27 19:09:57 2006 +0100
+++ b/src/HOL/ROOT.ML	Wed Dec 27 19:09:58 2006 +0100
@@ -37,11 +37,6 @@
 
 with_path "Integ" use_thy "Main";
 
-structure Main =
-struct
-  val thy = theory "Main"
-end;
-
 path_add "~~/src/HOL/Library";
 
 Goal "True";  (*leave subgoal package empty*)