src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 56303 4cc3f4db3447
parent 55452 29ec8680e61f
child 57037 c51132be8e16
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4                        reraise exn
     1.5                      else
     1.6                        (unknownN, fn () => "Internal error:\n" ^
     1.7 -                                          ML_Compiler.exn_message exn ^ "\n"))
     1.8 +                                          Runtime.exn_message exn ^ "\n"))
     1.9          val _ =
    1.10            (* The "expect" argument is deliberately ignored if the prover is
    1.11               missing so that the "Metis_Examples" can be processed on any