--- a/src/Pure/Isar/token.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/token.ML Fri Sep 25 20:37:59 2015 +0200
@@ -498,7 +498,7 @@
| SOME (Typ T) => Syntax.pretty_typ ctxt T
| SOME (Term t) => Syntax.pretty_term ctxt t
| SOME (Fact (_, ths)) =>
- Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
+ Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
| _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
fun pretty_src ctxt src =