diff -r 7667a85b53f1 -r e7951b191048 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Aug 28 16:04:51 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Aug 28 16:04:52 2005 +0200
@@ -60,7 +60,6 @@
     string * bool -> (string * typ * mixfix) list -> syntax -> syntax
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val merge_syntaxes: syntax -> syntax -> syntax
-  val type_syn: syntax
   val pure_syn: syntax
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
@@ -295,10 +294,12 @@
   end;
 
 
-(* type_syn *)
+(* pure_syn *)
 
-val type_syn = empty_syntax |> extend_syntax default_mode TypeExt.type_ext;
-val pure_syn = type_syn |> extend_syntax default_mode SynExt.pure_ext;
+val pure_syn =
+  empty_syntax
+  |> extend_syntax default_mode TypeExt.type_ext
+  |> extend_syntax default_mode SynExt.pure_ext;