src/Pure/Syntax/mixfix.ML
changeset 42293 6cca0343ea48
parent 42288 2074b31650e6
child 42297 140f283266b7
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 16:38:46 2011 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 17:45:37 2011 +0200
     1.3 @@ -88,7 +88,8 @@
     1.4  
     1.5  (* syn_ext_types *)
     1.6  
     1.7 -fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
     1.8 +val typeT = Type ("type", []);
     1.9 +fun make_type n = replicate n typeT ---> typeT;
    1.10  
    1.11  fun syn_ext_types type_decls =
    1.12    let
    1.13 @@ -150,8 +151,7 @@
    1.14        |> map (Syntax_Ext.stamp_trfun binder_stamp o
    1.15            apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
    1.16    in
    1.17 -    Syntax_Ext.syn_ext' true is_logtype
    1.18 -      mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    1.19 +    Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    1.20    end;
    1.21  
    1.22  end;