# HG changeset patch
# User wenzelm
# Date 1280851818 -7200
# Node ID dc65ed8bbb43d6e17d0f3fe3e8ea4f82a79ee699
# Parent  6fda94059baa37663f420d5083f9225282ff45cf
find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);

diff -r 6fda94059baa -r dc65ed8bbb43 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