1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jun 29 15:13:39 2005 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 29 15:13:40 2005 +0200
     1.3 @@ -42,27 +42,27 @@
     1.4        xprods: xprod list,
     1.5        consts: string list,
     1.6        prmodes: string list,
     1.7 -      parse_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
     1.8 +      parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
     1.9        parse_rules: (Ast.ast * Ast.ast) list,
    1.10 -      parse_translation: (string * ((term list -> term) * stamp)) list,
    1.11 -      print_translation: (string * ((bool -> typ -> term list -> term) * stamp)) list,
    1.12 +      parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
    1.13 +      print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
    1.14        print_rules: (Ast.ast * Ast.ast) list,
    1.15 -      print_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.16 +      print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.17        token_translation: (string * string * (string -> string * real)) list}
    1.18    val mfix_args: string -> int
    1.19    val escape_mfix: string -> string
    1.20    val syn_ext': bool -> (string -> bool) -> mfix list ->
    1.21 -    string list -> (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    1.22 -    (string * ((term list -> term) * stamp)) list *
    1.23 -    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.24 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list
    1.25 +    string list -> (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.26 +    (string * ((theory -> term list -> term) * stamp)) list *
    1.27 +    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    1.28 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
    1.29      -> (string * string * (string -> string * real)) list
    1.30      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.31    val syn_ext: mfix list -> string list ->
    1.32 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    1.33 -    (string * ((term list -> term) * stamp)) list *
    1.34 -    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.35 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list
    1.36 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.37 +    (string * ((theory -> term list -> term) * stamp)) list *
    1.38 +    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    1.39 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
    1.40      -> (string * string * (string -> string * real)) list
    1.41      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.42    val syn_ext_const_names: string list -> syn_ext
    1.43 @@ -72,6 +72,11 @@
    1.44      (string * ((term list -> term) * stamp)) list *
    1.45      (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.46      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    1.47 +  val syn_ext_advanced_trfuns:
    1.48 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.49 +    (string * ((theory -> term list -> term) * stamp)) list *
    1.50 +    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    1.51 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    1.52    val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    1.53    val standard_token_markers: string list
    1.54    val pure_ext: syn_ext
    1.55 @@ -323,12 +328,12 @@
    1.56      xprods: xprod list,
    1.57      consts: string list,
    1.58      prmodes: string list,
    1.59 -    parse_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.60 +    parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.61      parse_rules: (Ast.ast * Ast.ast) list,
    1.62 -    parse_translation: (string * ((term list -> term) * stamp)) list,
    1.63 -    print_translation: (string * ((bool -> typ -> term list -> term) * stamp)) list,
    1.64 +    parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
    1.65 +    print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
    1.66      print_rules: (Ast.ast * Ast.ast) list,
    1.67 -    print_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.68 +    print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.69      token_translation: (string * string * (string -> string * real)) list};
    1.70  
    1.71  
    1.72 @@ -361,9 +366,14 @@
    1.73  
    1.74  fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
    1.75  fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
    1.76 -fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
    1.77 +fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
    1.78  fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
    1.79  
    1.80 +fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
    1.81 +  let fun simple (name, (f, s)) = (name, (K f, s)) in
    1.82 +    syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
    1.83 +  end;
    1.84 +
    1.85  fun stamp_trfun s (c, f) = (c, (f, s));
    1.86  fun mk_trfun tr = stamp_trfun (stamp ()) tr;
    1.87  fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;