# HG changeset patch
# User wenzelm
# Date 1443201624 -7200
# Node ID 48ab72301c1edca168e74204a21b822feab50c65
# Parent  7bd1eb4b056eea87f579a2d6a0fde707fcb363e5
tuned;

diff -r 7bd1eb4b056e -r 48ab72301c1e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Sep 25 19:13:47 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Sep 25 19:20:24 2015 +0200
@@ -290,12 +290,8 @@
   (case undeclared_hyps context th of
     [] => th
   | undeclared =>
-      let
-        val ctxt = Context.cases Syntax.init_pretty_global I context;
-      in
-        error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
-          (map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared)))
-      end);
+      error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
+        (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared))));