src/HOL/Import/proof_kernel.ML
changeset 32091 30e2ffbba718
parent 31945 d5f186aa0bed
child 32174 9036cc8ae775
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4  
     1.5  val smart_string_of_thm = smart_string_of_cterm o cprop_of
     1.6  
     1.7 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
     1.8 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
     1.9  fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
    1.10  fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
    1.11  fun pth (HOLThm(ren,thm)) =