# HG changeset patch # User blanchet # Date 1348816370 -7200 # Node ID c44b2a404687c82e7349c34ba8fe7008489c1252 # Parent 9ce0c2cbadb8afe34db941d8bf2fc9a343c984d1 tuned message diff -r 9ce0c2cbadb8 -r c44b2a404687 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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