*** empty log message ***
authorwenzelm
Tue Nov 30 15:31:07 1993 +0100 (1993-11-30)
changeset 175c02750f7f604
parent 174 319ff2d6760b
child 176 5729f6757473
*** empty log message ***
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 12:12:18 1993 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 15:31:07 1993 +0100
     1.3 @@ -437,9 +437,9 @@
     1.4      val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
     1.5  
     1.6      val (syn1 as Syntax (ggr1, tabs1)) = 
     1.7 -      (case mk_xgram ext1 of
     1.8 -        xg1 as XGram {prods = [], ...} => 
     1.9 -          Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 xg1)
    1.10 +      (case ext1 of
    1.11 +        Ext {roots = [], mfix = [], ...} => 
    1.12 +          Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1))
    1.13        | _ => mk_syntax (ref (ExtGG (ggr0, ext1))));
    1.14  
    1.15      val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);