diff -r 128e122acc89 -r 1bf4e2cab673 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Nov 29 12:32:42 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Nov 29 13:51:37 1993 +0100
@@ -158,7 +158,7 @@
 
 (* mk_tables *)
 
-val mk_tables = extend_tables empty_tables;
+(* val mk_tables = extend_tables empty_tables; *)
 
 (* FIXME *)
 fun mk_tables (XGram xgram) =
@@ -426,7 +426,7 @@
 val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
 
 
-(* extend *)  (* FIXME *)
+(* extend *)  (* FIXME *) (* FIXME check *)
 
 fun old_extend syn read_ty (roots, xconsts, sext) =
   let
@@ -457,10 +457,10 @@
   end;
 
 
-fun extend syn read_ty (ex as (_, _, sext)) =
-  (case sext of
-    Sext {mixfix = [], ...} => new_extend
-  | NewSext {mixfix = [], ...} => new_extend
+fun extend syn read_ty (ex as (roots, _, sext)) =
+  (case (roots, sext) of
+    ([], Sext {mixfix = [], ...}) => new_extend
+  | ([], NewSext {mixfix = [], ...}) => new_extend
   | _ => old_extend) syn read_ty ex;