src/HOL/Import/proof_kernel.ML

 fun quotename c =
   if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
 
 fun simple_smart_string_of_cterm ctxt0 ct =
     let
-        val ctxt = Config.put show_all_types true ctxt0;
+        val ctxt = ctxt0
+          |> Config.put show_all_types true
+          |> Config.put Syntax.ambiguity_enabled true;
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
         val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
                            handle TERM _ => ct
     in
         quote (
         Print_Mode.setmp [] (
         setmp_CRITICAL show_brackets false (
-        setmp_CRITICAL Syntax.ambiguity_is_error false (
-        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))))
+        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
         ct)
     end
 
 exception SMART_STRING
 
-fun smart_string_of_cterm ctxt ct =
-    let
+fun smart_string_of_cterm ctxt0 ct =
+    let
+        val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false;
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
         val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
                    handle TERM _ => ct
         fun match u = t aconv u

             end
             handle ERROR mesg => F (n + 1)
               | SMART_STRING =>
                   error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
     in
-      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
-    end
-    handle ERROR mesg => simple_smart_string_of_cterm ctxt ct
+      Print_Mode.setmp [] F 0
+    end
+    handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct
 
 fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
 
 fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
 fun prin t = writeln (Print_Mode.setmp []