# HG changeset patch
# User blanchet
# Date 1407150978 -7200
# Node ID e1a3d025552d95ed249870d5656bea0599ff8852
# Parent  c5c388051840432f23e452694e98c16e8ae60070
tuned terminology (cf. 'isar_proofs' option)

diff -r c5c388051840 -r e1a3d025552d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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)