# HG changeset patch
# User wenzelm
# Date 1207826657 -7200
# Node ID d5ae46a8a716d344e0fae1d43c76e4ac866d2330
# Parent  f11515535c839f2b6cb028febf358c1ab5b4252c
finish: removed unnecessary Isar.init;

diff -r f11515535c83 -r d5ae46a8a716 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Thu Apr 10 13:24:15 2008 +0200
+++ b/src/Pure/Isar/session.ML	Thu Apr 10 13:24:17 2008 +0200
@@ -71,7 +71,6 @@
   (Output.accumulated_time ();
     ThyInfo.finish ();
     Present.finish ();
-    Toplevel.init_state ();
     session_finished := true);