1.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Dec 11 19:05:25 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Dec 11 21:39:26 2006 +0100
     1.3 @@ -42,33 +42,30 @@
     1.4        xprods: xprod list,
     1.5        consts: string list,
     1.6        prmodes: string list,
     1.7 -      parse_ast_translation:
     1.8 -        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
     1.9 +      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.10        parse_rules: (Ast.ast * Ast.ast) list,
    1.11 -      parse_translation:
    1.12 -        (string * ((Context.generic -> term list -> term) * stamp)) list,
    1.13 +      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    1.14        print_translation:
    1.15 -        (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
    1.16 +        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    1.17        print_rules: (Ast.ast * Ast.ast) list,
    1.18 -      print_ast_translation:
    1.19 -        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.20 +      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.21        token_translation: (string * string * (string -> string * real)) list}
    1.22    val mfix_delims: string -> string list
    1.23    val mfix_args: string -> int
    1.24    val escape_mfix: string -> string
    1.25    val unlocalize_mfix: string -> string
    1.26    val syn_ext': bool -> (string -> bool) -> mfix list ->
    1.27 -    string list -> (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.28 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
    1.29 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    1.30 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
    1.31 +    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.32 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    1.33 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    1.34 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    1.35      -> (string * string * (string -> string * real)) list
    1.36      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.37    val syn_ext: mfix list -> string list ->
    1.38 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.39 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
    1.40 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    1.41 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
    1.42 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.43 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    1.44 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    1.45 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    1.46      -> (string * string * (string -> string * real)) list
    1.47      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.48    val syn_ext_const_names: string list -> syn_ext
    1.49 @@ -79,10 +76,10 @@
    1.50      (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.51      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    1.52    val syn_ext_advanced_trfuns:
    1.53 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.54 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
    1.55 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    1.56 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    1.57 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    1.58 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    1.59 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    1.60 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    1.61    val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    1.62    val standard_token_markers: string list
    1.63    val pure_ext: syn_ext
    1.64 @@ -339,16 +336,13 @@
    1.65      xprods: xprod list,
    1.66      consts: string list,
    1.67      prmodes: string list,
    1.68 -    parse_ast_translation:
    1.69 -      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.70 +    parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.71      parse_rules: (Ast.ast * Ast.ast) list,
    1.72 -    parse_translation:
    1.73 -      (string * ((Context.generic -> term list -> term) * stamp)) list,
    1.74 +    parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    1.75      print_translation:
    1.76 -      (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
    1.77 +      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    1.78      print_rules: (Ast.ast * Ast.ast) list,
    1.79 -    print_ast_translation:
    1.80 -      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.81 +    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    1.82      token_translation: (string * string * (string -> string * real)) list};
    1.83  
    1.84