# HG changeset patch
# User haftmann
# Date 1193751577 -3600
# Node ID 001ab1d3f5679b76af686fc8a4f3b2eb7302b929
# Parent  ff5815d04c233e4b328e5b9c50b6c750c2a963eb
const antiquotation clarified

diff -r ff5815d04c23 -r 001ab1d3f567 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Oct 30 14:39:36 2007 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Oct 30 14:39:37 2007 +0100
@@ -440,8 +440,9 @@
 fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
 
 fun pretty_term_const ctxt t =
-  if Term.is_Const t then pretty_term ctxt t
-  else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
+  if Term.is_Const (singleton (Syntax.uncheck_terms ctxt) t)
+    then pretty_term ctxt t
+    else error ("Constant expected: " ^ Syntax.string_of_term ctxt t);
 
 fun pretty_abbrev ctxt t =
   let