--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat May 11 16:13:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat May 11 16:57:18 2013 +0200
@@ -58,11 +58,11 @@
fun parse_bool_option option name s =
(case s of
- "smart" => if option then NONE else raise Option
+ "smart" => if option then NONE else raise Option.Option
| "false" => SOME false
| "true" => SOME true
| "" => SOME true
- | _ => raise Option)
+ | _ => raise Option.Option)
handle Option.Option =>
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
error ("Parameter " ^ quote name ^ " must be assigned " ^