--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 04 13:13:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 04 13:16:18 2014 +0200
@@ -378,7 +378,7 @@
end)
else
one_line_params) ^
- (if isar_proofs = SOME true then "\n(No structured proof available -- proof too simple.)"
+ (if isar_proofs = SOME true then "\n(No Isar proof available.)"
else "")
| num_steps =>
let
@@ -387,7 +387,7 @@
(if do_preplay then [string_of_play_outcome play_outcome] else [])
in
one_line_proof_text ctxt 0 one_line_params ^
- "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+ "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
Active.sendback_markup [Markup.padding_command]
(string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
end)