1.1 --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Sun Oct 04 12:59:22 2009 +0200
     1.2 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Mon Oct 05 11:47:38 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
     1.5 -    ID:         $Id$
     1.6  
     1.7  Some rather large datatype examples (from John Harrison).
     1.8  *)
     1.9 @@ -8,9 +7,9 @@
    1.10  
    1.11  set timing;
    1.12  
    1.13 -warning "\nset quick_and_dirty\n"; set quick_and_dirty;
    1.14 +warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
    1.15  List.app time_use_thy tests;
    1.16  
    1.17 -warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
    1.18 +warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
    1.19  List.app ThyInfo.remove_thy tests;
    1.20  List.app time_use_thy tests;