| changeset 37900 | 8b3498b9eb4b |
| parent 33695 | bec342db1bf4 |
| child 38798 | 89f273ab1d42 |
--- 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;