src/Pure/System/session.ML
changeset 52083 f852d08376f9
parent 52080 02749038168b
child 52111 1fd184eaa310
--- a/src/Pure/System/session.ML	Mon May 20 14:04:21 2013 +0200
+++ b/src/Pure/System/session.ML	Mon May 20 15:42:14 2013 +0200
@@ -56,7 +56,6 @@
   Outer_Syntax.check_syntax ();
   Future.shutdown ();
   Event_Timer.shutdown ();
-  Options.reset_default ();
   session_finished := true);
 
 end;