# HG changeset patch
# User wenzelm
# Date 1216318513 -7200
# Node ID 4d7c96b72d494d077ae2874c2111742c521aa253
# Parent  9df10b28aa60f1dd365d0f4f65f3401624a21ac2
ThyInfo.remove_thy;

diff -r 9df10b28aa60 -r 4d7c96b72d49 Admin/Benchmarks/HOL-datatype/ROOT.ML
--- 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;