--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 02 15:10:18 2014 +0200
@@ -123,8 +123,8 @@
fun isar_proof_of () =
let
- val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
- atp_proof, goal) = try isar_params ()
+ val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
+ atp_proof, goal) = isar_params ()
val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0