author | wenzelm |
Wed, 21 Jul 2010 17:55:07 +0200 | |
changeset 37900 | 8b3498b9eb4b |
parent 37899 | 527cedd71356 |
child 37901 | ea7d4423cb5b |
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Wed Jul 21 17:46:36 2010 +0200 +++ b/Admin/Benchmarks/HOL-record/ROOT.ML Wed Jul 21 17:55:07 2010 +0200 @@ -8,7 +8,7 @@ Unsynchronized.set timing; warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty; -List.app time_use_thy tests; +use_thys tests; warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty; -List.app time_use_thy tests; +use_thys tests;