diff -r 0583db803066 -r a991d603aac6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 11 13:57:51 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 11 14:35:28 2013 +0100 @@ -373,7 +373,7 @@ fun hammer_away override_params subcommand opt_i fact_override state = let - (* this is necessary to avoid errors in jedit *) + (* necessary to avoid problems in jedit *) val state = state |> Proof.map_context (Config.put show_markup false) val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt)