src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 41743 d52af5722f0f
parent 41742 11e862c68b40
child 41746 e590971528b2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -36,11 +36,11 @@
      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    else
      "") ^
-  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
+  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
   (if blocking then
-     ""
+     "."
    else
-     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+     ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)