1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jan 04 00:12:30 2007 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jan 04 11:56:53 2007 +0100
     1.3 @@ -319,7 +319,7 @@
     1.4  fun print_exn_str NONE = NONE
     1.5    | print_exn_str (SOME (exn, s)) = SOME (cat_lines [exn_message exn, s]);
     1.6  
     1.7 -val print_exn_default = Option.app Output.error_msg o print_exn_str
     1.8 +val print_exn_default = K () o Option.map Output.error_msg o print_exn_str
     1.9  
    1.10  val print_exn_fn = ref print_exn_default;
    1.11  

     2.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Jan 04 00:12:30 2007 +0100
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Jan 04 11:56:53 2007 +0100
     2.3 @@ -110,7 +110,7 @@
     2.4    debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
     2.5    warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
     2.6    error_fn := (fn s => decorate "" "" "" s);
     2.7 -  Toplevel.print_exn_fn := (Option.app (decorate (special "364") (special "365") "*** ") o Toplevel.print_exn_str);
     2.8 +  Toplevel.print_exn_fn := (K () o Option.map (decorate (special "364") (special "365") "*** ") o Toplevel.print_exn_str);
     2.9    panic_fn := (fn s => decorate (special "364") (special "365") "!!! " s));
    2.10  
    2.11  

     3.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jan 04 00:12:30 2007 +0100
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jan 04 11:56:53 2007 +0100
     3.3 @@ -216,7 +216,7 @@
     3.4    warning_fn := (fn s => errormsg Nonfatal s);
     3.5    panic_fn := (fn s => errormsg Panic s);
     3.6    error_fn := (fn s => errormsg Nonfatal s); (* was (fn s => errormsg Fatal s); *)
     3.7 -  Toplevel.print_exn_fn := (Option.app (errormsg Fatal) o Toplevel.print_exn_str);
     3.8 +  Toplevel.print_exn_fn := (K () o Option.map (errormsg Fatal) o Toplevel.print_exn_str);
     3.9    ())
    3.10  
    3.11