src/HOL/Import/proof_kernel.ML
changeset 32174 9036cc8ae775
parent 32091 30e2ffbba718
child 32180 37800cb1d378
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Jul 24 20:55:56 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Jul 24 21:02:34 2009 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4  
     1.5  fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
     1.6  fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
     1.7 -fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
     1.8 +fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (OldGoals.the_context ()) t) ());
     1.9  fun pth (HOLThm(ren,thm)) =
    1.10      let
    1.11          (*val _ = writeln "Renaming:"