binder_tr: more informative exception;
authorwenzelm
Tue Mar 22 17:51:15 2011 +0100 (2011-03-22)
changeset 42055ad87c485ff30
parent 42054 8cd4783904d8
child 42056 160a630b2c7e
binder_tr: more informative exception;
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 16:39:34 2011 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Mar 22 17:51:15 2011 +0100
     1.3 @@ -112,11 +112,12 @@
     1.4  
     1.5  fun mk_binder_tr (syn, name) =
     1.6    let
     1.7 +    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
     1.8      fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
     1.9        | binder_tr [x, t] =
    1.10 -          let val abs = abs_tr [x, t] handle TERM _ => raise TERM ("binder_tr", [x, t])
    1.11 +          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
    1.12            in Lexicon.const name $ abs end
    1.13 -      | binder_tr ts = raise TERM ("binder_tr", ts);
    1.14 +      | binder_tr ts = err ts;
    1.15    in (syn, binder_tr) end;
    1.16  
    1.17