1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -562,7 +562,7 @@
     1.4    let
     1.5      val ctxt = Proof.context_of state;
     1.6      val prop = Syntax.read_prop ctxt s;
     1.7 -  in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
     1.8 +  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end;
     1.9  
    1.10  fun string_of_term state s =
    1.11    let
    1.12 @@ -571,15 +571,15 @@
    1.13      val T = Term.type_of t;
    1.14    in
    1.15      Pretty.string_of
    1.16 -      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
    1.17 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
    1.18 +      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
    1.19 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
    1.20    end;
    1.21  
    1.22  fun string_of_type state s =
    1.23    let
    1.24      val ctxt = Proof.context_of state;
    1.25      val T = ProofContext.read_typ ctxt s;
    1.26 -  in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
    1.27 +  in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
    1.28  
    1.29  fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
    1.30    PrintMode.with_modes modes (fn () =>