# HG changeset patch # User wenzelm # Date 1546543002 -3600 # Node ID a91e32843310817a2e7e4bf0bbcbabb14dc33119 # Parent b0568a9dd1607be13d723d5c1fa01925a8606973 tuned signature; diff -r b0568a9dd160 -r a91e32843310 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu Jan 03 16:53:18 2019 +0100 +++ b/src/Pure/Syntax/mixfix.ML Thu Jan 03 20:16:42 2019 +0100 @@ -164,7 +164,7 @@ val mfix = map mfix_of type_decls; val _ = map2 check_args type_decls mfix; val consts = map (fn (t, _, _) => (t, "")) type_decls; - in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end; + in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end; (* syn_ext_consts *) @@ -215,9 +215,7 @@ apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap); val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls; - in - Syntax_Ext.syn_ext' logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) - end; + in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end; end; diff -r b0568a9dd160 -r a91e32843310 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Thu Jan 03 16:53:18 2019 +0100 +++ b/src/Pure/Syntax/syntax_ext.ML Thu Jan 03 20:16:42 2019 +0100 @@ -33,18 +33,12 @@ val mfix_args: Symbol_Pos.T list -> int val mixfix_args: Input.source -> int val escape: string -> string - val syn_ext': string list -> mfix list -> + val syn_ext: string list -> mfix list -> (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext: mfix list -> (string * string) list -> - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * - (string * ((Proof.context -> term list -> term) * stamp)) list * - (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> - (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext val syn_ext_trfuns: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * @@ -406,7 +400,7 @@ (* syn_ext *) -fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) = +fun syn_ext logical_types mfixes consts trfuns (parse_rules, print_rules) = let val (parse_ast_translation, parse_translation, print_translation, print_ast_translation) = trfuns; @@ -429,10 +423,8 @@ end; -val syn_ext = syn_ext' []; - -fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; -fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []); +fun syn_ext_rules rules = syn_ext [] [] [] ([], [], [], []) rules; +fun syn_ext_trfuns trfuns = syn_ext [] [] [] trfuns ([], []); fun stamp_trfun s (c, f) = (c, (f, s)); fun mk_trfun tr = stamp_trfun (stamp ()) tr;