src/Pure/Isar/proof_display.ML
changeset 32145 220c9e439d39
parent 32091 30e2ffbba718
child 33389 bb3a5fa94a91
     1.1 --- a/src/Pure/Isar/proof_display.ML	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Jul 23 16:52:16 2009 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    let
     1.5      val thy = Thm.theory_of_thm th;
     1.6      val flags = {quote = true, show_hyps = false, show_status = true};
     1.7 -  in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
     1.8 +  in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end;
     1.9  
    1.10  val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
    1.11  val pp_term = Pretty.quote oo Syntax.pretty_term_global;