clarified implicit context;

--- a/src/Pure/display.ML	Sun Aug 30 15:43:13 2015 +0200
+++ b/src/Pure/display.ML	Sun Aug 30 17:32:36 2015 +0200
@@ -51,7 +51,9 @@
     val show_tags = Config.get ctxt show_tags;
     val show_hyps = Config.get ctxt show_hyps;
 
-    val th = Thm.strip_shyps raw_th handle Thm.CONTEXT _ => raw_th;
+    val th = raw_th
+      |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
+      |> perhaps (try Thm.strip_shyps);
 
     val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
     val extra_shyps = Thm.extra_shyps th;