# HG changeset patch
# User wenzelm
# Date 1440948756 -7200
# Node ID ed0a1067b1df3dce3bb62868124b3935d50774c5
# Parent  310cf33d548116aec9cff0bde162cbadafd37902
clarified implicit context;

diff -r 310cf33d5481 -r ed0a1067b1df src/Pure/display.ML
--- 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;