added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;

--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -464,13 +464,13 @@
           if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
       val case_constant = Constant (syntax (case_const dummyT))
       fun case_trans authentic =
-          (if authentic then ParsePrintRule else ParseRule)
+          (if authentic then Parse_Print_Rule else Parse_Rule)
             (app "_case_syntax"
               (Variable "x",
                foldr1 (app "_case2") (map_index (case1 authentic) spec)),
              capp (capps (case_constant, map_index arg1 spec), Variable "x"))
       fun one_abscon_trans authentic (n, c) =
-          (if authentic then ParsePrintRule else ParseRule)
+          (if authentic then Parse_Print_Rule else Parse_Rule)
             (cabs (con1 authentic n c, expvar n),
              capps (case_constant, map_index (when1 n) spec))
       fun abscon_trans authentic =
@@ -479,7 +479,7 @@
           case_trans false :: case_trans true ::
           abscon_trans false @ abscon_trans true
     in
-      val thy = Sign.add_trrules_i trans_rules thy
+      val thy = Sign.add_trrules trans_rules thy
     end
 
     (* prove beta reduction rule for case combinator *)

--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -24,9 +24,9 @@
 fun trans_rules name2 name1 n mx =
   let
     val vnames = Name.invents Name.context "a" n
-    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1)
+    val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
   in
-    [Syntax.ParsePrintRule
+    [Syntax.Parse_Print_Rule
       (Syntax.mk_appl (Constant name2) (map Variable vnames),
         fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
           vnames (Constant name1))] @
@@ -80,7 +80,7 @@
   in
     thy
     |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
-    |> Sign.add_trrules_i (maps #3 transformed_decls)
+    |> Sign.add_trrules (maps #3 transformed_decls)
   end
 
 in

--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Apr 03 21:59:33 2011 +0200
@@ -516,17 +516,17 @@
           val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
           val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
         in
-          [ParseRule (app_pat (capps (cname, xs)),
+          [Parse_Rule (app_pat (capps (cname, xs)),
                       mk_appl pname (map app_pat xs)),
-           ParseRule (app_var (capps (cname, xs)),
+           Parse_Rule (app_var (capps (cname, xs)),
                       app_var (args_list xs)),
-           PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
+           Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
                       app "_match" (mk_appl pname ps, args_list vs))]
         end;
       val trans_rules : Syntax.ast Syntax.trrule list =
           maps one_case_trans (pat_consts ~~ spec);
     in
-      val thy = Sign.add_trrules_i trans_rules thy;
+      val thy = Sign.add_trrules trans_rules thy;
     end;
 
     (* prove strictness and reduction rules of pattern combinators *)

--- a/src/Pure/General/position.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/General/position.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -34,6 +34,8 @@
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
+  type reports = (T * Markup.T) list
+  val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
   val str_of: T -> string
   type range = T * T
   val no_range: range
@@ -155,6 +157,13 @@
 fun report_text pos markup txt = Output.report (reported_text pos markup txt);
 fun report pos markup = report_text pos markup "";
 
+type reports = (T * Markup.T) list;
+
+fun reports _ [] _ _ = ()
+  | reports (r: reports Unsynchronized.ref) ps markup x =
+      let val ms = markup x
+      in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
+
 
 (* str_of *)
 

--- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -13,6 +13,8 @@
   val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val translations: (xstring * string) Syntax.trrule list -> theory -> theory
+  val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
@@ -154,6 +156,22 @@
 end;
 
 
+(* translation rules *)
+
+fun read_trrules thy raw_rules =
+  let
+    val ctxt = ProofContext.init_global thy;
+    val type_ctxt = ProofContext.type_context ctxt;
+    val syn = ProofContext.syn_of ctxt;
+  in
+    raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
+      Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s)))
+  end;
+
+fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
+fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
+
+
 (* oracles *)
 
 fun oracle (name, pos) (body_txt, body_pos) =

--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -175,9 +175,9 @@
     -- Parse.string;
 
 fun trans_arrow toks =
-  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
-    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
-    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
+  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
+    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
+    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
 
 val trans_line =
   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
@@ -185,11 +185,11 @@
 
 val _ =
   Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
 
 val _ =
   Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
-    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
+    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
 
 
 (* axioms and definitions *)

--- a/src/Pure/Isar/proof_context.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -65,7 +65,9 @@
   val allow_dummies: Proof.context -> Proof.context
   val check_tvar: Proof.context -> indexname * sort -> indexname * sort
   val check_tfree: Proof.context -> string * sort -> string * sort
-  val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term
+  val type_context: Proof.context -> Syntax.type_context
+  val term_context: Proof.context -> Syntax.term_context
+  val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
   val standard_infer_types: Proof.context -> term list -> term list
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
@@ -665,12 +667,18 @@
 
 in
 
+fun type_context ctxt : Syntax.type_context =
+ {get_class = read_class ctxt,
+  get_type = #1 o dest_Type o read_type_name_proper ctxt false,
+  markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
+  markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
+
 fun term_context ctxt : Syntax.term_context =
  {get_sort = get_sort ctxt,
   get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
     handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
   get_free = intern_skolem ctxt (Variable.def_type ctxt false),
-  markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x],
+  markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
   markup_free = fn x =>
     [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
     (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
@@ -748,14 +756,16 @@
 fun parse_sort ctxt text =
   let
     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
-    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
+    val S =
+      Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos)
       handle ERROR msg => parse_failed ctxt pos msg "sort";
   in Type.minimize_sort (tsig_of ctxt) S end;
 
 fun parse_typ ctxt text =
   let
     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
-    val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
+    val T =
+      Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos)
       handle ERROR msg => parse_failed ctxt pos msg "type";
   in T end;
 
@@ -777,8 +787,9 @@
     fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
-      Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos)
-        handle ERROR msg => parse_failed ctxt pos msg kind;
+      Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
+        root (syms, pos)
+      handle ERROR msg => parse_failed ctxt pos msg kind;
   in t end;
 
 
@@ -1079,13 +1090,6 @@
 
 (* authentic syntax *)
 
-val _ = Context.>>
-  (Context.map_theory
-    (Sign.add_advanced_trfuns
-      (Syntax.type_ast_trs
-        {read_class = read_class,
-          read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
-
 local
 
 fun const_ast_tr intern ctxt [Syntax.Variable c] =

--- a/src/Pure/Proof/proof_syntax.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -70,7 +70,7 @@
        (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
   |> Sign.add_modesyntax_i ("latex", false)
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
-  |> Sign.add_trrules_i (map Syntax.ParsePrintRule
+  |> Sign.add_trrules (map Syntax.Parse_Print_Rule
       [(Syntax.mk_appl (Constant "_Lam")
           [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
         Syntax.mk_appl (Constant "_Lam")

--- a/src/Pure/Syntax/syn_trans.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -48,6 +48,7 @@
     (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list *
     (string * (Ast.ast list -> Ast.ast)) list
+  type type_context
 end;
 
 signature SYN_TRANS =
@@ -57,8 +58,9 @@
   val prop_tr': term -> term
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val parsetree_to_ast: Proof.context -> bool ->
-    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
+  val parsetree_to_ast: Proof.context -> type_context -> bool ->
+    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
+    Parser.parsetree -> Position.reports * Ast.ast
   val ast_to_term: Proof.context ->
     (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
 end;
@@ -549,21 +551,44 @@
 
 (** parsetree_to_ast **)
 
-fun parsetree_to_ast ctxt constrain_pos trf =
+type type_context =
+ {get_class: string -> string,
+  get_type: string -> string,
+  markup_class: string -> Markup.T list,
+  markup_type: string -> Markup.T list};
+
+fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree =
   let
+    val {get_class, get_type, markup_class, markup_type} = type_context;
+
+    val reports = Unsynchronized.ref ([]: Position.reports);
+    fun report pos = Position.reports reports [pos];
+
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => f ctxt args);
 
-    fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
+    fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
+          let
+            val c = get_class (Lexicon.str_of_token tok);
+            val _ = report (Lexicon.pos_of_token tok) markup_class c;
+          in Ast.Constant (Lexicon.mark_class c) end
+      | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
+          let
+            val c = get_type (Lexicon.str_of_token tok);
+            val _ = report (Lexicon.pos_of_token tok) markup_type c;
+          in Ast.Constant (Lexicon.mark_type c) end
+      | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
           if constrain_pos then
             Ast.Appl [Ast.Constant "_constrain", ast_of pt,
               Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
           else ast_of pt
       | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
-  in ast_of end;
+
+    val ast = ast_of parsetree;
+  in (! reports, ast) end;
 
 
 

--- a/src/Pure/Syntax/syntax.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -116,17 +116,20 @@
   val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
-  val standard_parse_term: (term -> string option) -> term_context ->
-    Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term
-  val standard_parse_typ: Proof.context -> syntax ->
+  val standard_parse_term: (term -> string option) ->
+    Proof.context -> type_context -> term_context -> syntax ->
+    string -> Symbol_Pos.T list * Position.T -> term
+  val standard_parse_typ: Proof.context -> type_context -> syntax ->
     ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
-  val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
+  val standard_parse_sort: Proof.context -> type_context -> syntax ->
+    Symbol_Pos.T list * Position.T -> sort
   datatype 'a trrule =
-    ParseRule of 'a * 'a |
-    PrintRule of 'a * 'a |
-    ParsePrintRule of 'a * 'a
+    Parse_Rule of 'a * 'a |
+    Print_Rule of 'a * 'a |
+    Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val is_const: syntax -> string -> bool
+  val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
   val standard_unparse_term: {structs: string list, fixes: string list} ->
     {extern_class: string -> xstring, extern_type: string -> xstring,
       extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
@@ -149,10 +152,8 @@
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_const_gram: bool -> (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
-  val remove_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
-  val update_trrules_i: ast trrule list -> syntax -> syntax
-  val remove_trrules_i: ast trrule list -> syntax -> syntax
+  val update_trrules: ast trrule list -> syntax -> syntax
+  val remove_trrules: ast trrule list -> syntax -> syntax
 end;
 
 structure Syntax: SYNTAX =
@@ -619,8 +620,8 @@
 val basic_nonterms =
   (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
     Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
-    "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
-    "index", "struct", "id_position", "longid_position"]);
+    "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index",
+    "struct", "id_position", "longid_position", "type_name", "class_name"]);
 
 
 
@@ -711,7 +712,7 @@
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
-fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) =
+fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val toks = Lexicon.tokenize lexicon raw syms;
@@ -725,7 +726,8 @@
 
     val limit = Config.get ctxt ambiguity_limit;
     fun show_pt pt =
-      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt));
+      Pretty.string_of
+        (Ast.pretty_ast (#2 (Syn_Trans.parsetree_to_ast ctxt type_ctxt false (K NONE) pt)));
     val _ =
       if len <= Config.get ctxt ambiguity_level then ()
       else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
@@ -738,17 +740,18 @@
 
     val constrain_pos = not raw andalso Config.get ctxt positions;
   in
-    some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
+    some_results
+      (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
   end;
 
 
 (* read *)
 
-fun read ctxt (syn as Syntax (tabs, _)) root inp =
+fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
   let val {parse_ruletab, parse_trtab, ...} = tabs in
-    read_asts ctxt syn false root inp
-    |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab))
-    |> some_results (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab))
+    read_asts ctxt type_ctxt syn false root inp
+    |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
+    |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
   end;
 
 
@@ -790,51 +793,60 @@
             map (show_term o snd) (take limit results)))
       end;
 
-fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) =
-  read ctxt syn root (syms, pos)
+fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
+  read ctxt type_ctxt syn root (syms, pos)
   |> map (Type_Ext.decode_term term_ctxt)
   |> disambig ctxt check;
 
 
 (* read types *)
 
-fun standard_parse_typ ctxt syn get_sort (syms, pos) =
-  (case read ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
-    [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
+fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
+  (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
+    [res] =>
+      let val t = report_result ctxt res
+      in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
   | _ => error (ambiguity_msg pos));
 
 
 (* read sorts *)
 
-fun standard_parse_sort ctxt syn (syms, pos) =
-  (case read ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
-    [t] => Type_Ext.sort_of_term t
+fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
+  (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
+    [res] =>
+      let val t = report_result ctxt res
+      in Type_Ext.sort_of_term t end
   | _ => error (ambiguity_msg pos));
 
 
 
 (** prepare translation rules **)
 
+(* rules *)
+
 datatype 'a trrule =
-  ParseRule of 'a * 'a |
-  PrintRule of 'a * 'a |
-  ParsePrintRule of 'a * 'a;
+  Parse_Rule of 'a * 'a |
+  Print_Rule of 'a * 'a |
+  Parse_Print_Rule of 'a * 'a;
 
-fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
-  | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
-  | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
+fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y)
+  | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y)
+  | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y);
 
-fun parse_rule (ParseRule pats) = SOME pats
-  | parse_rule (PrintRule _) = NONE
-  | parse_rule (ParsePrintRule pats) = SOME pats;
+fun parse_rule (Parse_Rule pats) = SOME pats
+  | parse_rule (Print_Rule _) = NONE
+  | parse_rule (Parse_Print_Rule pats) = SOME pats;
 
-fun print_rule (ParseRule _) = NONE
-  | print_rule (PrintRule pats) = SOME (swap pats)
-  | print_rule (ParsePrintRule pats) = SOME (swap pats);
+fun print_rule (Parse_Rule _) = NONE
+  | print_rule (Print_Rule pats) = SOME (swap pats)
+  | print_rule (Parse_Print_Rule pats) = SOME (swap pats);
 
 
 fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
 
+
+(* check_rules *)
+
 local
 
 fun check_rule rule =
@@ -844,7 +856,18 @@
         Pretty.string_of (Ast.pretty_rule rule))
   | NONE => rule);
 
-fun read_pattern ctxt syn (root, str) =
+in
+
+fun check_rules rules =
+ (map check_rule (map_filter parse_rule rules),
+  map check_rule (map_filter print_rule rules));
+
+end;
+
+
+(* read_rule_pattern *)
+
+fun read_rule_pattern ctxt type_ctxt syn (root, str) =
   let
     fun constify (ast as Ast.Constant _) = ast
       | constify (ast as Ast.Variable x) =
@@ -854,25 +877,13 @@
 
     val (syms, pos) = read_token str;
   in
-    (case read_asts ctxt syn true root (syms, pos) of
-      [ast] => constify ast
+    (case read_asts ctxt type_ctxt syn true root (syms, pos) of
+      [res] =>
+        let val ast = report_result ctxt res
+        in constify ast end
     | _ => error (ambiguity_msg pos))
   end;
 
-fun prep_rules rd_pat raw_rules =
-  let val rules = map (map_trrule rd_pat) raw_rules in
-    (map check_rule (map_filter parse_rule rules),
-      map check_rule (map_filter print_rule rules))
-  end
-
-in
-
-val cert_rules = prep_rules I;
-
-fun read_rules ctxt syn = prep_rules (read_pattern ctxt syn);
-
-end;
-
 
 
 (** unparse terms, typs, sorts **)
@@ -920,14 +931,8 @@
 fun update_const_gram add is_logtype prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
 
-fun update_trrules ctxt syn =
-  ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt syn;
-
-fun remove_trrules ctxt syn =
-  remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt syn;
-
-val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
-val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
+val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules;
+val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules;
 
 
 (*export parts of internal Syntax structures*)

--- a/src/Pure/Syntax/type_ext.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -13,14 +13,10 @@
   val strip_positions: term -> term
   val strip_positions_ast: Ast.ast -> Ast.ast
   type term_context
-  val decode_term: term_context -> term -> (Position.T * Markup.T) list * term
+  val decode_term: term_context -> Position.reports * term -> Position.reports * term
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
   val no_type_brackets: unit -> bool
-  val type_ast_trs:
-   {read_class: Proof.context -> string -> string,
-    read_type: Proof.context -> string -> string} ->
-    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
 end;
 
 signature TYPE_EXT =
@@ -140,16 +136,13 @@
   markup_free: string -> Markup.T list,
   markup_var: indexname -> Markup.T list};
 
-fun decode_term (term_context: term_context) tm =
+fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
   let
     val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
-    val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
-    fun report [] _ _ = ()
-      | report ps markup x =
-          let val ms = markup x
-          in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
+    val reports = Unsynchronized.ref reports0;
+    fun report ps = Position.reports reports ps;
 
     fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
           (case decode_position typ of
@@ -252,30 +245,14 @@
 
 (* parse ast translations *)
 
-val class_ast = Ast.Constant o Lexicon.mark_class;
-val type_ast = Ast.Constant o Lexicon.mark_type;
-
-fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
-  | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
-
-fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
-      Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
-  | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
+fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
+  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
 
-fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
-  | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
-
-fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
-      Ast.Appl [type_ast (read_type c), ty]
-  | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
+  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
 
-fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
-      Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
-  | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
-
-fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
-      Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
-  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
+fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
+  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
 
 
 (* print ast translations *)
@@ -296,32 +273,35 @@
 
 (* type_ext *)
 
-val sortT = Type ("sort", []);
-val classesT = Type ("classes", []);
-val typesT = Type ("types", []);
+fun typ c = Type (c, []);
+
+val class_nameT = typ "class_name";
+val type_nameT = typ "type_name";
+
+val sortT = typ "sort";
+val classesT = typ "classes";
+val typesT = typ "types";
 
 local open Lexicon Syn_Ext in
 
 val type_ext = syn_ext' false (K false)
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
-   Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
-   Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
+   Mfix ("_",           type_nameT --> typeT,          "", [], max_pri),
+   Mfix ("_",           idT --> type_nameT,            "_type_name", [], max_pri),
+   Mfix ("_",           longidT --> type_nameT,        "_type_name", [], max_pri),
    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
    Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
-   Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
-   Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
+   Mfix ("_",           class_nameT --> sortT,         "", [], max_pri),
+   Mfix ("_",           idT --> class_nameT,           "_class_name", [], max_pri),
+   Mfix ("_",           longidT --> class_nameT,       "_class_name", [], max_pri),
    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
-   Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
-   Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
-   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
-   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
-   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
-   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
-   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
-   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
+   Mfix ("_",           class_nameT --> classesT,      "", [], max_pri),
+   Mfix ("_,_",         [class_nameT, classesT] ---> classesT, "_classes", [], max_pri),
+   Mfix ("_ _",         [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
+   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri),
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
@@ -329,18 +309,12 @@
    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   ["_type_prop"]
-  ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
+  (map Syn_Ext.mk_trfun
+    [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
+   [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   []
   ([], []);
 
-fun type_ast_trs {read_class, read_type} =
- [("_class_name", class_name_tr o read_class),
-  ("_classes", classes_tr o read_class),
-  ("_type_name", type_name_tr o read_type),
-  ("_tapp", tapp_ast_tr o read_type),
-  ("_tappl", tappl_ast_tr o read_type),
-  ("_bracket", K bracket_ast_tr)];
-
 end;
 
 end;

--- a/src/Pure/sign.ML	Sun Apr 03 18:17:21 2011 +0200
+++ b/src/Pure/sign.ML	Sun Apr 03 21:59:33 2011 +0200
@@ -108,10 +108,8 @@
     (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
   val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
     -> theory -> theory
-  val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
-  val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
-  val add_trrules_i: ast Syntax.trrule list -> theory -> theory
-  val del_trrules_i: ast Syntax.trrule list -> theory -> theory
+  val add_trrules: ast Syntax.trrule list -> theory -> theory
+  val del_trrules: ast Syntax.trrule list -> theory -> theory
   val new_group: theory -> theory
   val reset_group: theory -> theory
   val add_path: string -> theory -> theory
@@ -497,14 +495,8 @@
 
 (* translation rules *)
 
-fun gen_trrules f args thy = thy |> map_syn (fn syn =>
-  let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
-  in f (ProofContext.init_global thy) syn rules syn end);
-
-val add_trrules = gen_trrules Syntax.update_trrules;
-val del_trrules = gen_trrules Syntax.remove_trrules;
-val add_trrules_i = map_syn o Syntax.update_trrules_i;
-val del_trrules_i = map_syn o Syntax.remove_trrules_i;
+val add_trrules = map_syn o Syntax.update_trrules;
+val del_trrules = map_syn o Syntax.remove_trrules;
 
 
 (* naming *)