--- a/src/Pure/goal.ML Mon Aug 30 15:09:20 2010 +0200
+++ b/src/Pure/goal.ML Mon Aug 30 15:19:39 2010 +0200
@@ -159,7 +159,7 @@
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
SOME th => Drule.implies_intr_list casms
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
- | NONE => error "Tactic failed.");
+ | NONE => error "Tactic failed");
(* prove_common etc. *)
@@ -191,7 +191,7 @@
fun result () =
(case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
- NONE => err "Tactic failed."
+ NONE => err "Tactic failed"
| SOME st =>
let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]