diff -r 1169c65e9698 -r e5f4075d4c5e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jan 11 14:34:11 2014 +0100
+++ b/src/Pure/goal.ML	Sat Jan 11 17:05:03 2014 +0100
@@ -168,8 +168,7 @@
 
 fun prove_internal ctxt casms cprop tac =
   (case SINGLE (tac (map (Assumption.assume ctxt) casms)) (init cprop) of
-    SOME th => Drule.implies_intr_list casms
-      (finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
+    SOME th => Drule.implies_intr_list casms (finish ctxt th)
   | NONE => error "Tactic failed");