flipped global_names default;
authorwenzelm
Mon Oct 27 15:43:53 1997 +0100 (1997-10-27)
changeset 4011c161162bc8c5
parent 4010 59cac65fb751
child 4012 6adc18bd0009
flipped global_names default;
src/Pure/Thy/thy_parse.ML
     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 -- --$$ $$-- ^^;