src/HOLCF/IMP/ROOT.ML
changeset 5210 54aaa779b6b4
parent 3954 c8c188655948
child 6217 9dac1ee185e3
--- a/src/HOLCF/IMP/ROOT.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOLCF/IMP/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -4,8 +4,6 @@
     Copyright   1997  TU Muenchen
 *)
 
-reset global_names;
-
 (*Load theories from ../meta_theory without generating HTML files
   (has already been done by HOL/IMP/ROOT.ML)*)
 val old_make_html = !make_html;