src/Pure/Thy/thy_parse.ML
changeset 4011 c161162bc8c5
parent 3977 9b3cbfd6a936
child 4020 f88775cc8d17
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Oct 27 15:43:16 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 27 15:43:53 1997 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  *)
     1.5  
     1.6  (* FIXME tmp *)
     1.7 -val global_names = ref true;
     1.8 +val global_names = ref false;
     1.9  
    1.10  
    1.11  infix 5 -- --$$ $$-- ^^;