--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 28 09:12:49 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 28 09:12:50 2012 +0200
@@ -278,7 +278,7 @@
| SOME s => case s |> space_explode " " |> map Real.fromString of
[SOME r1, SOME r2] => (r1, r2)
| _ => error ("Parameter " ^ quote name ^
- "must be assigned a pair of floating-point \
+ " must be assigned a pair of floating-point \
\values (e.g., \"0.6 0.95\")")
fun lookup_option lookup' name =
case lookup name of