# HG changeset patch
# User wenzelm
# Date 911210791 -3600
# Node ID 975c984526b0af87e836706d154b7b78b321df18
# Parent  c8096461f5c8825c0614811de535bc8cc53ff38c
tuned names;

diff -r c8096461f5c8 -r 975c984526b0 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 16 11:06:15 1998 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 16 11:06:31 1998 +0100
@@ -7,9 +7,8 @@
 
 signature BASIC_OUTER_SYNTAX =
 sig
-  val print_outer_syntax: unit -> unit
   val main: unit -> unit
-  val main_loop: unit -> unit
+  val loop: unit -> unit
   val help: unit -> unit
 end;
 
@@ -20,6 +19,7 @@
   type parser
   val parser: bool -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
+  val print_outer_syntax: unit -> unit
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
   val get_header: Position.T -> (string, 'a) Source.source -> (bstring * bstring list) option
@@ -168,20 +168,20 @@
 
 (** the read-eval-print loop **)
 
-fun main_loop () = (Context.reset_context (); Toplevel.loop isar);
+fun loop () = (Context.reset_context (); Toplevel.loop isar);
 
 fun main () =
  (Toplevel.set_state Toplevel.toplevel;
   ml_prompts "ML> " "ML# ";
   writeln ("\n\n" ^ Context.welcome ());
-  main_loop ());
+  loop ());
 
 
 (* help *)
 
 fun help () =
   writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\
-    \invoke 'main_loop();' to enter the Isar loop.");
+    \invoke 'loop();' to enter the Isar loop.");
 
 
 end;