1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4                             handle TERM _ => ct)
     1.5      in
     1.6          quote (
     1.7 -        PrintMode.setmp [] (
     1.8 +        Print_Mode.setmp [] (
     1.9          setmp_CRITICAL show_brackets false (
    1.10          setmp_CRITICAL show_all_types true (
    1.11          setmp_CRITICAL Syntax.ambiguity_is_error false (
    1.12 @@ -239,14 +239,14 @@
    1.13                | SMART_STRING =>
    1.14                    error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
    1.15      in
    1.16 -      PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    1.17 +      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    1.18      end
    1.19      handle ERROR mesg => simple_smart_string_of_cterm ct
    1.20  
    1.21  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    1.22  
    1.23 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
    1.24 -fun prin t = writeln (PrintMode.setmp []
    1.25 +fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
    1.26 +fun prin t = writeln (Print_Mode.setmp []
    1.27    (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
    1.28  fun pth (HOLThm(ren,thm)) =
    1.29      let