src/Pure/Syntax/mixfix.ML
changeset 14903 d264b8ad3eec
parent 14855 a58abaad4f45
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Jun 09 18:54:07 2004 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Jun 09 18:54:26 2004 +0200
     1.3 @@ -42,10 +42,8 @@
     1.4  signature MIXFIX =
     1.5  sig
     1.6    include MIXFIX1
     1.7 -  val syn_ext_types: string list -> (string * int * mixfix) list
     1.8 -    -> SynExt.syn_ext
     1.9 -  val syn_ext_consts: string list -> (string * typ * mixfix) list
    1.10 -    -> SynExt.syn_ext
    1.11 +  val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
    1.12 +  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
    1.13  end;
    1.14  
    1.15  
    1.16 @@ -133,7 +131,7 @@
    1.17  
    1.18  (* syn_ext_types *)
    1.19  
    1.20 -fun syn_ext_types logtypes type_decls =
    1.21 +fun syn_ext_types type_decls =
    1.22    let
    1.23      fun name_of (t, _, mx) = type_name t mx;
    1.24  
    1.25 @@ -151,17 +149,17 @@
    1.26          | (sy, 2, Infix p) => Some (mk_infix sy t (p + 1) (p + 1) p)
    1.27          | (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p)
    1.28          | (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p)
    1.29 -        | _ => error ("Bad mixfix declaration for type " ^ quote t))
    1.30 +        | _ => error ("Bad mixfix declaration for type: " ^ quote t))
    1.31        end;
    1.32  
    1.33      val mfix = mapfilter mfix_of type_decls;
    1.34      val xconsts = map name_of type_decls;
    1.35 -  in SynExt.syn_ext logtypes mfix xconsts ([], [], [], []) [] ([], []) end;
    1.36 +  in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
    1.37  
    1.38  
    1.39  (* syn_ext_consts *)
    1.40  
    1.41 -fun syn_ext_consts logtypes const_decls =
    1.42 +fun syn_ext_consts is_logtype const_decls =
    1.43    let
    1.44      fun name_of (c, _, mx) = const_name c mx;
    1.45  
    1.46 @@ -171,7 +169,7 @@
    1.47  
    1.48      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    1.49            [Type ("idts", []), ty2] ---> ty3
    1.50 -      | binder_typ c _ = error ("Bad type of binder " ^ quote c);
    1.51 +      | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
    1.52  
    1.53      fun mfix_of decl =
    1.54        let val c = name_of decl in
    1.55 @@ -198,7 +196,10 @@
    1.56      val binder_trs = map SynTrans.mk_binder_tr binders;
    1.57      val binder_trs' =
    1.58        map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;
    1.59 -  in SynExt.syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) end;
    1.60 +  in
    1.61 +    SynExt.syn_ext' true is_logtype
    1.62 +      mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
    1.63 +  end;
    1.64  
    1.65  
    1.66