--- 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;