# HG changeset patch
# User wenzelm
# Date 754669867 -3600
# Node ID c02750f7f604f4feeba81000b0fd93a5db4c4f32
# Parent  319ff2d6760b40446df354781bbdc2ddb09d3da6
*** empty log message ***

diff -r 319ff2d6760b -r c02750f7f604 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 12:12:18 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 15:31:07 1993 +0100
@@ -437,9 +437,9 @@
     val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
 
     val (syn1 as Syntax (ggr1, tabs1)) = 
-      (case mk_xgram ext1 of
-        xg1 as XGram {prods = [], ...} => 
-          Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 xg1)
+      (case ext1 of
+        Ext {roots = [], mfix = [], ...} => 
+          Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1))
       | _ => mk_syntax (ref (ExtGG (ggr0, ext1))));
 
     val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);