1.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Sep 05 22:23:48 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 05 23:16:21 2010 +0200
     1.3 @@ -190,6 +190,7 @@
     1.4  fun simple_smart_string_of_cterm ctxt0 ct =
     1.5      let
     1.6          val ctxt = ctxt0
     1.7 +          |> Config.put show_brackets false
     1.8            |> Config.put show_all_types true
     1.9            |> Config.put show_sorts true
    1.10            |> Config.put Syntax.ambiguity_enabled true;
    1.11 @@ -198,10 +199,7 @@
    1.12          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    1.13                             handle TERM _ => ct
    1.14      in
    1.15 -        quote (
    1.16 -        Print_Mode.setmp [] (
    1.17 -        setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
    1.18 -        ct)
    1.19 +        quote (Print_Mode.setmp [] (Syntax.string_of_term ctxt o Thm.term_of) ct)
    1.20      end
    1.21  
    1.22  exception SMART_STRING
    1.23 @@ -215,14 +213,14 @@
    1.24                     handle TERM _ => ct
    1.25          fun match u = t aconv u
    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 1 f ctxt x = G 0 f (Config.put show_brackets true ctxt) x
    1.29            | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
    1.30 -          | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x
    1.31 +          | G 3 f ctxt x = G 2 f (Config.put show_brackets true ctxt) x
    1.32            | G _ _ _ _ = raise SMART_STRING
    1.33          fun F n =
    1.34              let
    1.35                  val str =
    1.36 -                  setmp_CRITICAL show_brackets false (G n Syntax.string_of_term ctxt) (term_of ct)
    1.37 +                  G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
    1.38                  val u = Syntax.parse_term ctxt str
    1.39                    |> Type_Infer.constrain T |> Syntax.check_term ctxt
    1.40              in