1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Sep 03 21:13:53 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 03 22:36:16 2010 +0200
     1.3 @@ -189,7 +189,9 @@
     1.4  
     1.5  fun simple_smart_string_of_cterm ctxt0 ct =
     1.6      let
     1.7 -        val ctxt = Config.put show_all_types true ctxt0;
     1.8 +        val ctxt = ctxt0
     1.9 +          |> Config.put show_all_types true
    1.10 +          |> Config.put Syntax.ambiguity_enabled true;
    1.11          val {t,T,...} = rep_cterm ct
    1.12          (* Hack to avoid parse errors with Trueprop *)
    1.13          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    1.14 @@ -198,15 +200,15 @@
    1.15          quote (
    1.16          Print_Mode.setmp [] (
    1.17          setmp_CRITICAL show_brackets false (
    1.18 -        setmp_CRITICAL Syntax.ambiguity_is_error false (
    1.19 -        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))))
    1.20 +        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
    1.21          ct)
    1.22      end
    1.23  
    1.24  exception SMART_STRING
    1.25  
    1.26 -fun smart_string_of_cterm ctxt ct =
    1.27 +fun smart_string_of_cterm ctxt0 ct =
    1.28      let
    1.29 +        val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false;
    1.30          val {t,T,...} = rep_cterm ct
    1.31          (* Hack to avoid parse errors with Trueprop *)
    1.32          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    1.33 @@ -232,9 +234,9 @@
    1.34                | SMART_STRING =>
    1.35                    error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
    1.36      in
    1.37 -      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    1.38 +      Print_Mode.setmp [] F 0
    1.39      end
    1.40 -    handle ERROR mesg => simple_smart_string_of_cterm ctxt ct
    1.41 +    handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct
    1.42  
    1.43  fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
    1.44