# HG changeset patch
# User wenzelm
# Date 1087716424 -7200
# Node ID b1ecb7859c9979938668fefbed0686a4a81a57ce
# Parent  0613f64653b7b2e005e0a3502acaa7ee50b05e32
avoid premature evaluation of syn_of (wastes time in conjunction with pp);

diff -r 0613f64653b7 -r b1ecb7859c99 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 20 09:26:48 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 20 09:27:04 2004 +0200
@@ -375,19 +375,20 @@
 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
   syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
 
-
 end;
 
 
 
 (** pretty printing **)
 
-fun pretty_term ctxt = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) o context_tr' ctxt;
-val pretty_typ = Sign.pretty_typ o sign_of;
-val pretty_sort = Sign.pretty_sort o sign_of;
+fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) (context_tr' ctxt t);
+fun pretty_typ ctxt T = Sign.pretty_typ (sign_of ctxt) T;
+fun pretty_sort ctxt S = Sign.pretty_sort (sign_of ctxt) S;
+fun pretty_classrel ctxt cs = Sign.pretty_classrel (sign_of ctxt) cs;
+fun pretty_arity ctxt ar = Sign.pretty_arity (sign_of ctxt) ar;
 
-fun pp ctxt = Pretty.pp (pretty_term ctxt) (pretty_typ ctxt) (pretty_sort ctxt)
-  (Sign.pretty_classrel (sign_of ctxt)) (Sign.pretty_arity (sign_of ctxt));
+fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt,
+  pretty_classrel ctxt, pretty_arity ctxt);
 
 val string_of_term = Pretty.string_of oo pretty_term;
 
diff -r 0613f64653b7 -r b1ecb7859c99 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Jun 20 09:26:48 2004 +0200
+++ b/src/Pure/sign.ML	Sun Jun 20 09:27:04 2004 +0200
@@ -599,7 +599,7 @@
     (exists (equal CPureN o !) stamps)
     (if ! NameSpace.long_names then t else extrn_term spaces t);
 
-fun pretty_term sg = pretty_term' (syn_of sg) sg;
+fun pretty_term sg t = pretty_term' (syn_of sg) sg t;
 
 fun pretty_typ sg T =
   Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
@@ -631,8 +631,8 @@
 fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
 fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
 
-fun pp sg = Pretty.pp (pretty_term sg) (pretty_typ sg) (pretty_sort sg)
-  (pretty_classrel sg) (pretty_arity sg);
+fun pp sg = Pretty.pp (pretty_term sg, pretty_typ sg, pretty_sort sg,
+  pretty_classrel sg, pretty_arity sg);