src/Pure/Thy/thy_output.ML
changeset 25241 001ab1d3f567
parent 25054 b15a9a5dc9fe
child 25373 ccbf65080fdf
equal deleted inserted replaced
25240:ff5815d04c23 25241:001ab1d3f567
   438   Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
   438   Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
   439 
   439 
   440 fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
   440 fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
   441 
   441 
   442 fun pretty_term_const ctxt t =
   442 fun pretty_term_const ctxt t =
   443   if Term.is_Const t then pretty_term ctxt t
   443   if Term.is_Const (singleton (Syntax.uncheck_terms ctxt) t)
   444   else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
   444     then pretty_term ctxt t
       
   445     else error ("Constant expected: " ^ Syntax.string_of_term ctxt t);
   445 
   446 
   446 fun pretty_abbrev ctxt t =
   447 fun pretty_abbrev ctxt t =
   447   let
   448   let
   448     fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
   449     fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
   449     val (head, args) = Term.strip_comb t;
   450     val (head, args) = Term.strip_comb t;