src/Pure/Thy/thy_output.ML
changeset 25241 001ab1d3f567
parent 25054 b15a9a5dc9fe
child 25373 ccbf65080fdf
--- 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