diff -r 8cd4783904d8 -r ad87c485ff30 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 16:39:34 2011 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 17:51:15 2011 +0100
@@ -112,11 +112,12 @@
 
 fun mk_binder_tr (syn, name) =
   let
+    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
       | binder_tr [x, t] =
-          let val abs = abs_tr [x, t] handle TERM _ => raise TERM ("binder_tr", [x, t])
+          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
           in Lexicon.const name $ abs end
-      | binder_tr ts = raise TERM ("binder_tr", ts);
+      | binder_tr ts = err ts;
   in (syn, binder_tr) end;