tuned;
authorwenzelm
Sun Nov 26 18:07:34 2006 +0100 (2006-11-26)
changeset 2153507f8cd0d7962
parent 21534 68f805e9db0b
child 21536 f119c730f509
tuned;
src/Pure/Syntax/syn_trans.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Sun Nov 26 18:07:33 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sun Nov 26 18:07:34 2006 +0100
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5  (* binder *)
     1.6  
     1.7 -fun mk_binder_tr (sy, name) =
     1.8 +fun mk_binder_tr (syn, name) =
     1.9    let
    1.10      fun tr (Free (x, T), t) = Lexicon.const name $ Term.absfree (x, T, t)
    1.11        | tr (Const ("_idtdummy", T), t) = Lexicon.const name $ Term.absdummy (T, t)
    1.12 @@ -116,9 +116,9 @@
    1.13        | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
    1.14        | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);
    1.15  
    1.16 -    fun binder_tr (*sy*) [idts, body] = tr (idts, body)
    1.17 -      | binder_tr (*sy*) ts = raise TERM ("binder_tr", ts);
    1.18 -  in (sy, binder_tr) end;
    1.19 +    fun binder_tr [idts, body] = tr (idts, body)
    1.20 +      | binder_tr ts = raise TERM ("binder_tr", ts);
    1.21 +  in (syn, binder_tr) end;
    1.22  
    1.23  
    1.24  (* meta propositions *)
    1.25 @@ -292,7 +292,7 @@
    1.26  
    1.27  (* binder *)
    1.28  
    1.29 -fun mk_binder_tr' (name, sy) =
    1.30 +fun mk_binder_tr' (name, syn) =
    1.31    let
    1.32      fun mk_idts [] = raise Match    (*abort translation*)
    1.33        | mk_idts [idt] = idt
    1.34 @@ -301,13 +301,11 @@
    1.35      fun tr' t =
    1.36        let
    1.37          val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
    1.38 -      in Lexicon.const sy $ mk_idts xs $ bd end;
    1.39 +      in Lexicon.const syn $ mk_idts xs $ bd end;
    1.40  
    1.41 -    fun binder_tr' (*name*) (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
    1.42 -      | binder_tr' (*name*) [] = raise Match;
    1.43 -  in
    1.44 -    (name, binder_tr')
    1.45 -  end;
    1.46 +    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Lexicon.const name $ t), ts)
    1.47 +      | binder_tr' [] = raise Match;
    1.48 +  in (name, binder_tr') end;
    1.49  
    1.50  
    1.51  (* idtyp constraints *)