src/Pure/System/isar.ML

--- a/src/Pure/System/isar.ML	Mon May 31 19:36:13 2010 +0200
+++ b/src/Pure/System/isar.ML	Mon May 31 21:06:57 2010 +0200
@@ -72,7 +72,7 @@
 
 fun find_and_undo _ [] = error "Undo history exhausted"
   | find_and_undo which ((prev, tr) :: hist) =
-      ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
+      ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());
         if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
 
 in