identify binder translations only once (admits remove);
authorwenzelm
Sat Apr 16 18:57:53 2005 +0200 (2005-04-16)
changeset 1575165e4790c7914
parent 15750 860c282e6ca6
child 15752 8cdc6249044b
identify binder translations only once (admits remove);
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sat Apr 16 18:57:39 2005 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat Apr 16 18:57:53 2005 +0200
     1.3 @@ -45,8 +45,7 @@
     1.4    val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
     1.5  end;
     1.6  
     1.7 -
     1.8 -structure Mixfix : MIXFIX =
     1.9 +structure Mixfix: MIXFIX =
    1.10  struct
    1.11  
    1.12  
    1.13 @@ -158,6 +157,8 @@
    1.14  
    1.15  (* syn_ext_consts *)
    1.16  
    1.17 +val binder_stamp = stamp ();
    1.18 +
    1.19  fun syn_ext_consts is_logtype const_decls =
    1.20    let
    1.21      fun name_of (c, _, mx) = const_name c mx;
    1.22 @@ -192,9 +193,9 @@
    1.23      val mfix = List.concat (map mfix_of const_decls);
    1.24      val xconsts = map name_of const_decls;
    1.25      val binders = List.mapPartial binder const_decls;
    1.26 -    val binder_trs = map SynTrans.mk_binder_tr binders;
    1.27 -    val binder_trs' =
    1.28 -      map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;
    1.29 +    val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o SynTrans.mk_binder_tr);
    1.30 +    val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o
    1.31 +        apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap);
    1.32    in
    1.33      SynExt.syn_ext' true is_logtype
    1.34        mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])