find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
--- a/src/Pure/System/isar.ML Tue Aug 03 16:57:45 2010 +0200
+++ b/src/Pure/System/isar.ML Tue Aug 03 18:10:18 2010 +0200
@@ -68,8 +68,7 @@
fun find_and_undo _ [] = error "Undo history exhausted"
| find_and_undo which ((prev, tr) :: hist) =
- ((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);
+ if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
in