--- 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 -- --$$ $$-- ^^;