const antiquotation clarified
authorhaftmann
Tue Oct 30 14:39:37 2007 +0100 (2007-10-30)
changeset 25241001ab1d3f567
parent 25240 ff5815d04c23
child 25242 6c3890cbceac
const antiquotation clarified
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Oct 30 14:39:36 2007 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Oct 30 14:39:37 2007 +0100
     1.3 @@ -440,8 +440,9 @@
     1.4  fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
     1.5  
     1.6  fun pretty_term_const ctxt t =
     1.7 -  if Term.is_Const t then pretty_term ctxt t
     1.8 -  else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
     1.9 +  if Term.is_Const (singleton (Syntax.uncheck_terms ctxt) t)
    1.10 +    then pretty_term ctxt t
    1.11 +    else error ("Constant expected: " ^ Syntax.string_of_term ctxt t);
    1.12  
    1.13  fun pretty_abbrev ctxt t =
    1.14    let