1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -429,22 +429,23 @@
     1.4  
     1.5  val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
     1.6  
     1.7 -fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     1.8 +fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
     1.9 +
    1.10  fun pretty_term_abbrev ctxt =
    1.11    ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
    1.12  
    1.13  fun pretty_term_typ ctxt t =
    1.14 -  ProofContext.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
    1.15 +  Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
    1.16  
    1.17 -fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
    1.18 +fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
    1.19  
    1.20  fun pretty_term_const ctxt t =
    1.21    if Term.is_Const t then pretty_term ctxt t
    1.22 -  else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
    1.23 +  else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
    1.24  
    1.25  fun pretty_abbrev ctxt t =
    1.26    let
    1.27 -    fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
    1.28 +    fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
    1.29      val (head, args) = Term.strip_comb t;
    1.30      val (c, T) = Term.dest_Const head handle TERM _ => err ();
    1.31      val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
    1.32 @@ -519,7 +520,7 @@
    1.33    ("typeof", args Args.term (output pretty_term_typeof)),
    1.34    ("const", args Args.term (output pretty_term_const)),
    1.35    ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
    1.36 -  ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
    1.37 +  ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
    1.38    ("text", args (Scan.lift Args.name) (output (K pretty_text))),
    1.39    ("goals", output_goals true),
    1.40    ("subgoals", output_goals false),