src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 56303 4cc3f4db3447
parent 56081 72fad75baf7e
child 56985 82c83978fbd9
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4            |> (fn {outcome, used_facts} => (outcome, used_facts))
     1.5            handle exn =>
     1.6              if Exn.is_interrupt exn then reraise exn
     1.7 -            else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
     1.8 +            else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
     1.9  
    1.10          val death = Timer.checkRealTimer timer
    1.11          val outcome0 = if is_none outcome0 then SOME outcome else outcome0