src/Pure/Syntax/mixfix.ML
changeset 42298 d622145603ee
parent 42297 140f283266b7
child 52143 36ffe23b25f8
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:11:29 2011 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 22:40:29 2011 +0200
     1.3 @@ -110,8 +110,8 @@
     1.4  
     1.5      val mfix = map mfix_of type_decls;
     1.6      val _ = map2 check_args type_decls mfix;
     1.7 -    val xconsts = map #1 type_decls;
     1.8 -  in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
     1.9 +    val consts = map (fn (t, _, _) => (t, "")) type_decls;
    1.10 +  in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end;
    1.11  
    1.12  
    1.13  (* syn_ext_consts *)
    1.14 @@ -143,15 +143,16 @@
    1.15        | binder _ = NONE;
    1.16  
    1.17      val mfix = maps mfix_of const_decls;
    1.18 -    val xconsts = map #1 const_decls;
    1.19      val binders = map_filter binder const_decls;
    1.20      val binder_trs = binders
    1.21        |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
    1.22      val binder_trs' = binders
    1.23        |> map (Syntax_Ext.stamp_trfun binder_stamp o
    1.24            apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
    1.25 +
    1.26 +    val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
    1.27    in
    1.28 -    Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    1.29 +    Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
    1.30    end;
    1.31  
    1.32  end;