# HG changeset patch
# User wenzelm
# Date 754657938 -3600
# Node ID 319ff2d6760b40446df354781bbdc2ddb09d3da6
# Parent  85071e6ad29538b54b1d0648c24a24a28cdbf302
*** empty log message ***

diff -r 85071e6ad295 -r 319ff2d6760b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 30 11:08:18 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Nov 30 12:12:18 1993 +0100
@@ -430,12 +430,17 @@
 
 (* extend *)  (* FIXME *)
 
-fun old_extend syn read_ty (roots, xconsts, sext) =
+fun extend syn read_ty (roots, xconsts, sext) =
   let
-    val Syntax (ggr0, Tabs {roots = roots0, ...}) = syn;
+    val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
 
     val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
-    val (syn1 as Syntax (ggr1, tabs1)) = mk_syntax (ref (ExtGG (ggr0, ext1)));
+
+    val (syn1 as Syntax (ggr1, tabs1)) = 
+      (case mk_xgram ext1 of
+        xg1 as XGram {prods = [], ...} => 
+          Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 xg1)
+      | _ => mk_syntax (ref (ExtGG (ggr0, ext1))));
 
     val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
     val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
@@ -444,28 +449,6 @@
   end;
 
 
-fun new_extend syn read_ty (roots, xconsts, sext) =
-  let
-    val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
-
-    val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
-    val (syn1 as Syntax (ggr1, tabs1)) =
-      Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1));
-
-    val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
-    val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
-  in
-    Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
-  end;
-
-
-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;
-
-
 (* merge *)
 
 fun merge roots syn1 syn2 =