# HG changeset patch
# User wenzelm
# Date 877344618 -7200
# Node ID c8c188655948b2b8f7dd74e4da0599a45e5e3d3f
# Parent  473ea5ce5ca8d491b20a2ad17890d63adc209ea5
reset global_names;

diff -r 473ea5ce5ca8 -r c8c188655948 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Mon Oct 20 12:47:44 1997 +0200
+++ b/src/FOL/ROOT.ML	Mon Oct 20 12:50:18 1997 +0200
@@ -11,6 +11,8 @@
 
 writeln banner;
 
+reset global_names;
+
 print_depth 1;  
 
 use "../Provers/simplifier.ML";
diff -r 473ea5ce5ca8 -r c8c188655948 src/HOLCF/IMP/ROOT.ML
--- a/src/HOLCF/IMP/ROOT.ML	Mon Oct 20 12:47:44 1997 +0200
+++ b/src/HOLCF/IMP/ROOT.ML	Mon Oct 20 12:50:18 1997 +0200
@@ -4,6 +4,8 @@
     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;