src/Pure/Isar/outer_syntax.ML
changeset 44186 806f0ec1a43d
parent 43712 3c2c912af2ef
child 44187 88d770052bac
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:20:36 2011 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:41:29 2011 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    type isar
     1.5    val isar: TextIO.instream -> bool -> isar
     1.6    val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
     1.7 -  val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
     1.8 +  val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     1.9      (Toplevel.transition * Toplevel.transition list) list
    1.10    val prepare_command: Position.T -> string -> Toplevel.transition
    1.11  end;
    1.12 @@ -224,7 +224,7 @@
    1.13  fun process_file path thy =
    1.14    let
    1.15      val trs = parse (Path.position path) (File.read path);
    1.16 -    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
    1.17 +    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
    1.18      val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
    1.19    in
    1.20      (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of