# HG changeset patch
# User wenzelm
# Date 1236089572 -3600
# Node ID 11373ba06bf0c679733e224fd37c748704851b1f
# Parent  9224f88c16514d577b28a6c4c6ccc487e686dea2
Binding.str_of;
removed dead code;
tuned;

diff -r 9224f88c1651 -r 11373ba06bf0 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Mar 03 15:09:09 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Mar 03 15:12:52 2009 +0100
@@ -91,14 +91,10 @@
     fun match_bind (n, b) = (n = Binding.base_name b);
     fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
       (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
-      (Binding.base_name b1 = Binding.base_name b2) andalso
-      (if mx1 = mx2 then true
-      else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^
-                    " in expression."));
+      Binding.base_name b1 = Binding.base_name b2 andalso
+        (mx1 = mx2 orelse
+          error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
       
-    fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
-      (* FIXME: cannot compare bindings for equality. *)
-
     fun params_loc loc =
       (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
     fun params_inst (expr as (loc, (prfx, Positional insts))) =