# HG changeset patch
# User wenzelm
# Date 877963433 -3600
# Node ID c161162bc8c593d47ad45daee8d5b70d321e02dc
# Parent  59cac65fb751590ce9f41e36378ccdfd496ef57e
flipped global_names default;

diff -r 59cac65fb751 -r c161162bc8c5 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Oct 27 15:43:16 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 27 15:43:53 1997 +0100
@@ -6,7 +6,7 @@
 *)
 
 (* FIXME tmp *)
-val global_names = ref true;
+val global_names = ref false;
 
 
 infix 5 -- --$$ $$-- ^^;