1.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -191,6 +191,7 @@
     1.4      let
     1.5          val ctxt = ctxt0
     1.6            |> Config.put show_all_types true
     1.7 +          |> Config.put show_sorts true
     1.8            |> Config.put Syntax.ambiguity_enabled true;
     1.9          val {t,T,...} = rep_cterm ct
    1.10          (* Hack to avoid parse errors with Trueprop *)
    1.11 @@ -199,8 +200,7 @@
    1.12      in
    1.13          quote (
    1.14          Print_Mode.setmp [] (
    1.15 -        setmp_CRITICAL show_brackets false (
    1.16 -        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
    1.17 +        setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
    1.18          ct)
    1.19      end
    1.20  
    1.21 @@ -214,7 +214,7 @@
    1.22          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    1.23                     handle TERM _ => ct
    1.24          fun match u = t aconv u
    1.25 -        fun G 0 f ctxt x = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true) (f ctxt) x
    1.26 +        fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
    1.27            | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
    1.28            | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
    1.29            | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x