src/Pure/Syntax/syn_trans.ML
changeset 42055 ad87c485ff30
parent 42053 006095137a81
child 42057 3eba96ff3d3e
equal deleted inserted replaced
42054:8cd4783904d8 42055:ad87c485ff30
   110 
   110 
   111 (* binder *)
   111 (* binder *)
   112 
   112 
   113 fun mk_binder_tr (syn, name) =
   113 fun mk_binder_tr (syn, name) =
   114   let
   114   let
       
   115     fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
   115     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
   116     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
   116       | binder_tr [x, t] =
   117       | binder_tr [x, t] =
   117           let val abs = abs_tr [x, t] handle TERM _ => raise TERM ("binder_tr", [x, t])
   118           let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
   118           in Lexicon.const name $ abs end
   119           in Lexicon.const name $ abs end
   119       | binder_tr ts = raise TERM ("binder_tr", ts);
   120       | binder_tr ts = err ts;
   120   in (syn, binder_tr) end;
   121   in (syn, binder_tr) end;
   121 
   122 
   122 
   123 
   123 (* type propositions *)
   124 (* type propositions *)
   124 
   125