# HG changeset patch
# User wenzelm
# Date 1215704860 -7200
# Node ID 4bbf70c35a6e499fbd84e54ab0c0fdd1e860e658
# Parent  02b2c9eab4e2f43903d14ef1a220389ffbb3f27a
tuned;

diff -r 02b2c9eab4e2 -r 4bbf70c35a6e src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Thu Jul 10 17:43:02 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Thu Jul 10 17:47:40 2008 +0200
@@ -142,7 +142,6 @@
 end;
 
 fun set_point id = change_point (K id);
-fun init_point () = set_point no_id;
 
 fun point_result () = NAMED_CRITICAL "Isar" (fn () =>
   let val id = point () in (id, the_result id) end);
@@ -243,7 +242,7 @@
 
 fun toplevel_loop {init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  if init then (init_point (); init_commands ()) else ();
+  if init then (set_point no_id; init_commands ()) else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
 
@@ -251,6 +250,7 @@
 
 fun loop () =
   toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
+
 fun main () =
   toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};