# HG changeset patch
# User wenzelm
# Date 1283718228 -7200
# Node ID b0b3b6318e3bd7a074daa56457d6ede88a2196a1
# Parent  6f5f64542405549730f20c42b9229acf466d93d6
Syntax.standard_parse_term: eliminated redundant Pretty.pp;

diff -r 6f5f64542405 -r b0b3b6318e3b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 05 22:15:50 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 05 22:23:48 2010 +0200
@@ -763,7 +763,7 @@
     fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
-      Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
+      Syntax.standard_parse_term check get_sort map_const map_free
         ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
       handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
   in t end;
diff -r 6f5f64542405 -r b0b3b6318e3b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Sep 05 22:15:50 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Sep 05 22:23:48 2010 +0200
@@ -114,7 +114,7 @@
   val ambiguity_level_value: Config.value Config.T
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
-  val standard_parse_term: Pretty.pp -> (term -> string option) ->
+  val standard_parse_term: (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> bool * string) -> (string -> string option) -> Proof.context ->
     (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
@@ -743,8 +743,8 @@
 (* read terms *)
 
 (*brute-force disambiguation via type-inference*)
-fun disambig _ _ _ [t] = t
-  | disambig ctxt pp check ts =
+fun disambig _ _ [t] = t
+  | disambig ctxt check ts =
       let
         val level = Config.get ctxt ambiguity_level;
         val limit = Config.get ctxt ambiguity_limit;
@@ -759,6 +759,8 @@
         val errs = Par_List.map check ts;
         val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
         val len = length results;
+
+        val show_term = setmp_CRITICAL Printer.show_brackets true (string_of_term ctxt);
       in
         if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
         else if len = 1 then
@@ -770,13 +772,13 @@
         else cat_error (ambig_msg ()) (cat_lines
           (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of_term pp) (take limit results)))
+            map show_term (take limit results)))
       end;
 
-fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
+fun standard_parse_term check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
   read ctxt is_logtype syn ty (syms, pos)
   |> map (Type_Ext.decode_term get_sort map_const map_free)
-  |> disambig ctxt (Printer.pp_show_brackets pp) check;
+  |> disambig ctxt check;
 
 
 (* read types *)