pprint: proper global context via Syntax.init_pretty_global;
authorwenzelm
Sun May 18 15:04:43 2008 +0200 (2008-05-18)
changeset 26949a9a1ebfb4d23
parent 26948 efe3e0e235d6
child 26950 80366b6eb94c
pprint: proper global context via Syntax.init_pretty_global;
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Sun May 18 15:04:41 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Sun May 18 15:04:43 2008 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4      Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
     1.5    else Pretty.str "<context>");
     1.6  
     1.7 -fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
     1.8 +fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
     1.9  
    1.10  val pprint_typ = pprint Syntax.pretty_typ;
    1.11  val pprint_term = pprint Syntax.pretty_term;