author | wenzelm |
Thu, 17 Jul 2008 20:15:13 +0200 | |
changeset 27641 | 4d7c96b72d49 |
parent 27640 | 9df10b28aa60 |
child 27642 | c0db1220b071 |
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Thu Jul 17 20:15:12 2008 +0200 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Thu Jul 17 20:15:13 2008 +0200 @@ -12,5 +12,5 @@ List.app time_use_thy tests; warning "\nreset quick_and_dirty\n"; reset quick_and_dirty; -List.app remove_thy tests; +List.app ThyInfo.remove_thy tests; List.app time_use_thy tests;