# HG changeset patch
# User wenzelm
# Date 1329474279 -3600
# Node ID fbb3c68a8d3c0208f6c32218be4d64c17b5633e4
# Parent  696f3fec3f836218fa1fa0313069311af1f867bb
retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);

diff -r 696f3fec3f83 -r fbb3c68a8d3c src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 23:07:01 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 17 11:24:39 2012 +0100
@@ -198,7 +198,6 @@
 fun smart_string_of_cterm ctxt0 ct =
     let
         val ctxt = ctxt0
-          |> Config.put Syntax.ambiguity "warning"  (* FIXME actually "error" (!?) *)
           |> Config.put show_brackets false
           |> Config.put show_all_types false
           |> Config.put show_types false