# 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);