find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
authorwenzelm
Tue, 03 Aug 2010 18:10:18 +0200
changeset 38138 dc65ed8bbb43
parent 38137 6fda94059baa
child 38139 ac94ff28e9e1
find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
src/Pure/System/isar.ML
--- 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