# HG changeset patch
# User wenzelm
# Date 1268141387 -3600
# Node ID 69e1740fbfb12215dc667e2d4ff33e0ba04eb9ed
# Parent  aa59452c913c2cb3eda017590298f0177c1a8dcd
simplified Syntax.basic_syntax (again);
separate Syntax.type_ast_trs depending on read_class/read_type;

diff -r aa59452c913c -r 69e1740fbfb1 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Mar 09 14:55:25 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 09 14:29:47 2010 +0100
@@ -29,10 +29,7 @@
   val mode_default: mode
   val mode_input: mode
   val merge_syntaxes: syntax -> syntax -> syntax
-  val empty_syntax: syntax
-  val basic_syntax:
-   {read_class: theory -> xstring -> string,
-    read_type: theory -> xstring -> string} -> syntax
+  val basic_syntax: syntax
   val basic_nonterms: string list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
@@ -383,9 +380,9 @@
 
 (* basic syntax *)
 
-fun basic_syntax read =
+val basic_syntax =
   empty_syntax
-  |> update_syntax mode_default (TypeExt.type_ext read)
+  |> update_syntax mode_default TypeExt.type_ext
   |> update_syntax mode_default SynExt.pure_ext;
 
 val basic_nonterms =
diff -r aa59452c913c -r 69e1740fbfb1 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Mar 09 14:55:25 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Mar 09 14:29:47 2010 +0100
@@ -15,6 +15,10 @@
   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 =
@@ -23,9 +27,7 @@
   val term_of_sort: sort -> term
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val sortT: typ
-  val type_ext:
-   {read_class: theory -> string -> string,
-    read_type: theory -> string -> string} -> SynExt.syn_ext
+  val type_ext: SynExt.syn_ext
 end;
 
 structure TypeExt: TYPE_EXT =
@@ -240,7 +242,7 @@
 
 local open Lexicon SynExt in
 
-fun type_ext {read_class, read_type} = syn_ext' false (K false)
+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),
@@ -267,19 +269,18 @@
    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   ["_type_prop"]
-  (map SynExt.mk_trfun
-   [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
-    ("_classes", classes_tr o read_class o ProofContext.theory_of),
-    ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
-    ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),
-    ("_tappl", tappl_ast_tr o read_type o ProofContext.theory_of),
-    ("_bracket", K bracket_ast_tr)],
-   [],
-   [],
-   map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
+  ([], [], [], map SynExt.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;