src/Pure/Isar/isar_output.ML
changeset 15960 9bd6550dc004
parent 15918 6d6d3fabef02
child 15988 181bbcee76f5
     1.1 --- a/src/Pure/Isar/isar_output.ML	Fri May 13 20:21:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_output.ML	Sat May 14 21:31:13 2005 +0200
     1.3 @@ -360,11 +360,15 @@
     1.4  fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt;
     1.5  
     1.6  fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c)
     1.7 -  | pretty_term_const ctxt term = raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
     1.8 +  | pretty_term_const ctxt term =
     1.9 +      raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
    1.10  
    1.11  fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
    1.12  
    1.13 -fun pretty_term_style ctxt (name, term) = pretty_term ctxt ((Style.get_style (ProofContext.theory_of ctxt) name) term);
    1.14 +fun pretty_term_style ctxt (name, term) =
    1.15 +  let
    1.16 +    val thy = ProofContext.theory_of ctxt
    1.17 +  in pretty_term ctxt (TermStyle.lookup_style thy name ctxt term) end;
    1.18  
    1.19  fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm);
    1.20