1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Dec 21 00:40:16 2001 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Dec 21 00:40:52 2001 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    val prems_of: context -> thm list
     1.5    val print_proof_data: theory -> unit
     1.6    val init: theory -> context
     1.7 +  val add_syntax: (string * typ option * mixfix option) list -> context -> context
     1.8    val is_fixed: context -> string -> bool
     1.9    val default_type: context -> string -> typ option
    1.10    val used_types: context -> string list
    1.11 @@ -98,13 +99,13 @@
    1.12    val fix: (string list * string option) list -> context -> context
    1.13    val fix_i: (string list * typ option) list -> context -> context
    1.14    val fix_direct: (string list * typ option) list -> context -> context
    1.15 +  val add_fixes: (string * typ option * mixfix option) list -> context -> context
    1.16    val fix_frees: term list -> context -> context
    1.17    val bind_skolem: context -> string list -> term -> term
    1.18    val get_case: context -> string -> string option list -> RuleCases.T
    1.19    val add_cases: (string * RuleCases.T) list -> context -> context
    1.20    val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
    1.21    val show_hyps: bool ref
    1.22 -  val add_syntax: (string * typ option * mixfix option) list -> context -> context
    1.23    val pretty_term: context -> term -> Pretty.T
    1.24    val pretty_typ: context -> typ -> Pretty.T
    1.25    val pretty_sort: context -> sort -> Pretty.T
    1.26 @@ -333,13 +334,13 @@
    1.27    | struct_tr _ ts = raise TERM ("struct_tr", ts);
    1.28  
    1.29  
    1.30 -(* add_syntax and syn_of *)
    1.31 +(* add syntax *)
    1.32 +
    1.33 +fun mixfix_type mx = replicate (Syntax.mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
    1.34  
    1.35  local
    1.36  
    1.37 -val aT = TFree ("'a", logicS);
    1.38 -
    1.39 -fun mixfix x None mx = (fixedN ^ x, replicate (Syntax.mixfix_args mx) aT ---> aT, mx)
    1.40 +fun mixfix x None mx = (fixedN ^ x, mixfix_type mx, mx)
    1.41    | mixfix x (Some T) mx = (fixedN ^ x, T, mx);
    1.42  
    1.43  fun prep_mixfix (_, _, None) = None
    1.44 @@ -1120,11 +1121,15 @@
    1.45      ctxt' |> add xs Ts
    1.46    end;
    1.47  
    1.48 +fun prep_type (x, None, Some mx) = ([x], Some (mixfix_type mx))
    1.49 +  | prep_type (x, opt_T, _) = ([x], opt_T);
    1.50 +
    1.51  in
    1.52  
    1.53  val fix = gen_fix read_vars add_vars;
    1.54  val fix_i = gen_fix cert_vars add_vars;
    1.55  val fix_direct = gen_fix cert_vars add_vars_direct;
    1.56 +fun add_fixes decls = add_syntax decls o fix_direct (map prep_type decls);
    1.57  
    1.58  end;
    1.59