src/Pure/Syntax/syntax.ML
changeset 175 c02750f7f604
parent 174 319ff2d6760b
child 237 a7d3e712767a
--- 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);