src/HOL/ex/svc_funcs.ML
changeset 15531 08c8dad8e399
parent 14982 ff1c919f4982
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/ex/svc_funcs.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -76,8 +76,8 @@
     1.4  			">/dev/null 2>&1"))
     1.5        val svc_output =
     1.6          (case Library.try File.read svc_output_file of
     1.7 -          Some out => out
     1.8 -        | None => error "SVC returned no output");
     1.9 +          SOME out => out
    1.10 +        | NONE => error "SVC returned no output");
    1.11    in
    1.12        if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    1.13        else (File.rm svc_input_file; File.rm svc_output_file);