src/Pure/Isar/outer_syntax.ML
changeset 15973 5fd94d84470f
parent 15830 74d8412b1a27
child 15989 80dd2f5780df
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue May 17 10:19:43 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue May 17 10:19:44 2005 +0200
     1.3 @@ -280,7 +280,7 @@
     1.4    Source.of_list toks
     1.5    |> toplevel_source false true true get_parser
     1.6    |> Source.exhaust
     1.7 -  |> map (fn tr => (Toplevel.name_of tr, valOf (Toplevel.source_of tr), tr));
     1.8 +  |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
     1.9  
    1.10  
    1.11  (** read theory **)
    1.12 @@ -299,7 +299,7 @@
    1.13      val pos = Path.position path;
    1.14      val (name', parents, files) = ThyHeader.scan (src, pos);
    1.15      val ml_path = ThyLoad.ml_path name;
    1.16 -    val ml_file = if ml andalso isSome (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.17 +    val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.18    in
    1.19      if name <> name' then
    1.20        error ("Filename " ^ quote (Path.pack path) ^