1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 23 19:50:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 23 19:50:51 2005 +0200
     1.3 @@ -7,10 +7,13 @@
     1.4  
     1.5  signature BASIC_OUTER_SYNTAX =
     1.6  sig
     1.7 -  val main: unit -> unit
     1.8 -  val loop: unit -> unit
     1.9 -  val sync_main: unit -> unit
    1.10 -  val sync_loop: unit -> unit
    1.11 +  structure Isar:
    1.12 +    sig
    1.13 +      val main: unit -> unit
    1.14 +      val loop: unit -> unit
    1.15 +      val sync_main: unit -> unit
    1.16 +      val sync_loop: unit -> unit
    1.17 +    end;
    1.18  end;
    1.19  
    1.20  signature OUTER_SYNTAX =
    1.21 @@ -376,10 +379,13 @@
    1.22    writeln (Session.welcome ());
    1.23    gen_loop term no_pos);
    1.24  
    1.25 -fun main () = gen_main false false;
    1.26 -fun loop () = gen_loop false false;
    1.27 -fun sync_main () = gen_main true true;
    1.28 -fun sync_loop () = gen_loop true true;
    1.29 +structure Isar =
    1.30 +struct
    1.31 +  fun main () = gen_main false false;
    1.32 +  fun loop () = gen_loop false false;
    1.33 +  fun sync_main () = gen_main true true;
    1.34 +  fun sync_loop () = gen_loop true true;
    1.35 +end;
    1.36  
    1.37  
    1.38  (*final declarations of this structure!*)
    1.39 @@ -387,7 +393,6 @@
    1.40  val markup_command = parser false o SOME;
    1.41  val improper_command = parser true NONE;
    1.42  
    1.43 -
    1.44  end;
    1.45  
    1.46  (*setup theory syntax dependent operations*)
    1.47 @@ -397,3 +402,4 @@
    1.48  
    1.49  structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
    1.50  open BasicOuterSyntax;
    1.51 +open Isar;