src/Pure/display.ML

--- a/src/Pure/display.ML	Sun Aug 30 15:21:25 2015 +0200
+++ b/src/Pure/display.ML	Sun Aug 30 15:43:13 2015 +0200
@@ -51,7 +51,7 @@
     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 = Thm.strip_shyps raw_th handle Thm.CONTEXT _ => raw_th;
 
     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;