# HG changeset patch
# User wenzelm
# Date 1164560854 -3600
# Node ID 07f8cd0d79625a286eb270d6da6fca32ba014854
# Parent  68f805e9db0bbee9b2491502d2e960e04a3d317d
tuned;

diff -r 68f805e9db0b -r 07f8cd0d7962 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sun Nov 26 18:07:33 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Nov 26 18:07:34 2006 +0100
@@ -105,7 +105,7 @@
 
 (* binder *)
 
-fun mk_binder_tr (sy, name) =
+fun mk_binder_tr (syn, name) =
   let
     fun tr (Free (x, T), t) = Lexicon.const name $ Term.absfree (x, T, t)
       | tr (Const ("_idtdummy", T), t) = Lexicon.const name $ Term.absdummy (T, t)
@@ -116,9 +116,9 @@
       | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
       | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);
 
-    fun binder_tr (*sy*) [idts, body] = tr (idts, body)
-      | binder_tr (*sy*) ts = raise TERM ("binder_tr", ts);
-  in (sy, binder_tr) end;
+    fun binder_tr [idts, body] = tr (idts, body)
+      | binder_tr ts = raise TERM ("binder_tr", ts);
+  in (syn, binder_tr) end;
 
 
 (* meta propositions *)
@@ -292,7 +292,7 @@
 
 (* binder *)
 
-fun mk_binder_tr' (name, sy) =
+fun mk_binder_tr' (name, syn) =
   let
     fun mk_idts [] = raise Match    (*abort translation*)
       | mk_idts [idt] = idt
@@ -301,13 +301,11 @@
     fun tr' t =
       let
         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
-      in Lexicon.const sy $ mk_idts xs $ bd end;
+      in Lexicon.const syn $ mk_idts xs $ bd end;
 
-    fun binder_tr' (*name*) (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
-      | binder_tr' (*name*) [] = raise Match;
-  in
-    (name, binder_tr')
-  end;
+    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
+      | binder_tr' [] = raise Match;
+  in (name, binder_tr') end;
 
 
 (* idtyp constraints *)