retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
authorwenzelm
Fri Feb 17 11:24:39 2012 +0100 (2012-02-17)
changeset 46511fbb3c68a8d3c
parent 46510 696f3fec3f83
child 46512 4f9f61f9b535
retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
src/HOL/Import/proof_kernel.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 23:07:01 2012 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 17 11:24:39 2012 +0100
     1.3 @@ -198,7 +198,6 @@
     1.4  fun smart_string_of_cterm ctxt0 ct =
     1.5      let
     1.6          val ctxt = ctxt0
     1.7 -          |> Config.put Syntax.ambiguity "warning"  (* FIXME actually "error" (!?) *)
     1.8            |> Config.put show_brackets false
     1.9            |> Config.put show_all_types false
    1.10            |> Config.put show_types false