prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
prefer non-strict lazy over strict future;

--- a/src/Pure/Syntax/parser.ML	Fri Nov 25 14:23:36 2011 +0100
+++ b/src/Pure/Syntax/parser.ML	Fri Nov 25 16:32:29 2011 +0100
@@ -9,7 +9,7 @@
   type gram
   val empty_gram: gram
   val extend_gram: Syntax_Ext.xprod list -> gram -> gram
-  val merge_gram: gram * gram -> gram
+  val make_gram: Syntax_Ext.xprod list -> gram
   val pretty_gram: gram -> Pretty.T list
   datatype parsetree =
     Node of string * parsetree list |
@@ -526,105 +526,7 @@
           prods = Array.vector prods'}
       end;
 
-
-(*Merge two grammars*)
-fun merge_gram (gram_a, gram_b) =
-  let
-    (*find out which grammar is bigger*)
-    val
-      (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
-        chains = chains1, lambdas = lambdas1, prods = prods1},
-      Gram {nt_count = nt_count2, prod_count = prod_count2, tags = tags2,
-        chains = chains2, lambdas = lambdas2, prods = prods2}) =
-      let
-        val Gram {prod_count = count_a, ...} = gram_a;
-        val Gram {prod_count = count_b, ...} = gram_b;
-      in
-        if count_a > count_b
-        then (gram_a, gram_b)
-        else (gram_b, gram_a)
-      end;
-
-    (*get existing tag from grammar1 or create a new one*)
-    fun get_tag nt_count tags nt =
-      (case Symtab.lookup tags nt of
-        SOME tag => (nt_count, tags, tag)
-      | NONE => (nt_count + 1, Symtab.update_new (nt, nt_count) tags, nt_count));
-
-    val ((nt_count1', tags1'), tag_table) =
-      let
-        val table = Array.array (nt_count2, ~1);
-
-        fun the_nt tag =
-          the (Symtab.get_first (fn (n, t) => if t = tag then SOME n else NONE) tags2);
-        fun store_tag nt_count tags ~1 = (nt_count, tags)
-          | store_tag nt_count tags tag =
-              let
-                val (nt_count', tags', tag') = get_tag nt_count tags (the_nt tag);
-                val _ = Array.update (table, tag, tag');
-              in store_tag nt_count' tags' (tag - 1) end;
-      in (store_tag nt_count1 tags1 (nt_count2 - 1), table) end;
-
-    (*convert grammar2 tag to grammar1 tag*)
-    fun convert_tag tag = Array.sub (tag_table, tag);
-
-    (*convert chain list to raw productions*)
-    fun mk_chain_prods [] result = result
-      | mk_chain_prods ((to, froms) :: cs) result =
-          let
-            val to_tag = convert_tag to;
-
-            fun make [] result = result
-              | make (from :: froms) result = make froms
-                  ((to_tag, ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
-          in mk_chain_prods cs (make froms [] @ result) end;
-
-    val chain_prods = mk_chain_prods chains2 [];
-
-    (*convert prods2 array to productions*)
-    fun process_nt ~1 result = result
-      | process_nt nt result =
-          let
-            val nt_prods = fold (union (op =) o snd) (snd (Vector.sub (prods2, nt))) [];
-            val lhs_tag = convert_tag nt;
-
-            (*convert tags in rhs*)
-            fun process_rhs [] result = result
-              | process_rhs (Terminal tk :: rhs) result =
-                  process_rhs rhs (result @ [Terminal tk])
-              | process_rhs (Nonterminal (nt, prec) :: rhs) result =
-                  process_rhs rhs (result @ [Nonterminal (convert_tag nt, prec)]);
-
-            (*convert tags in productions*)
-            fun process_prods [] result = result
-              | process_prods ((rhs, id, prec) :: ps) result =
-                  process_prods ps ((lhs_tag, (process_rhs rhs [], id, prec)) :: result);
-          in process_nt (nt - 1) (process_prods nt_prods [] @ result) end;
-
-    val raw_prods = chain_prods @ process_nt (nt_count2 - 1) [];
-
-    val prods1' =
-      let
-        fun get_prod i =
-          if i < nt_count1 then Vector.sub (prods1, i)
-          else (([], []), []);
-      in Array.tabulate (nt_count1', get_prod) end;
-
-    val fromto_chains = inverse_chains chains1 [];
-
-    val (fromto_chains', lambdas', SOME prod_count1') =
-      add_prods prods1' fromto_chains lambdas1 (SOME prod_count1) raw_prods;
-
-    val chains' = inverse_chains fromto_chains' [];
-  in
-    Gram
-     {nt_count = nt_count1',
-      prod_count = prod_count1',
-      tags = tags1',
-      chains = chains',
-      lambdas = lambdas',
-      prods = Array.vector prods1'}
-  end;
+fun make_gram xprods = extend_gram xprods empty_gram;
 
 
 

--- a/src/Pure/Syntax/syntax.ML	Fri Nov 25 14:23:36 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Nov 25 16:32:29 2011 +0100
@@ -74,7 +74,7 @@
   val string_of_sort_global: theory -> sort -> string
   type syntax
   val eq_syntax: syntax * syntax -> bool
-  val join_syntax: syntax -> unit
+  val force_syntax: syntax -> unit
   val lookup_const: syntax -> string -> string option
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -92,7 +92,7 @@
   val mode_default: mode
   val mode_input: mode
   val empty_syntax: syntax
-  val merge_syntaxes: syntax -> syntax -> syntax
+  val merge_syntax: syntax * syntax -> syntax
   val token_markers: string list
   val basic_nonterms: string list
   val print_gram: syntax -> unit
@@ -379,16 +379,11 @@
 
 (** datatype syntax **)
 
-fun future_gram deps e =
-  singleton
-    (Future.cond_forks {name = "Syntax.gram", group = NONE,
-      deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
-
 datatype syntax =
   Syntax of {
     input: Syntax_Ext.xprod list,
     lexicon: Scan.lexicon,
-    gram: Parser.gram future,
+    gram: Parser.gram lazy,
     consts: string Symtab.table,
     prmodes: string list,
     parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
@@ -401,12 +396,12 @@
 
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
 
-fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram);
+fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
 
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
-fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Future.join gram);
+fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Lazy.force gram);
 
 fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
 fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
@@ -427,7 +422,7 @@
 val empty_syntax = Syntax
   ({input = [],
     lexicon = Scan.empty_lexicon,
-    gram = Future.value Parser.empty_gram,
+    gram = Lazy.value Parser.empty_gram,
     consts = Symtab.empty,
     prmodes = [],
     parse_ast_trtab = Symtab.empty,
@@ -460,7 +455,7 @@
     Syntax
     ({input = new_xprods @ input,
       lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
-      gram = Future.value (Parser.extend_gram new_xprods (Future.join gram)),
+      gram = Lazy.value (Parser.extend_gram new_xprods (Lazy.force gram)),
       consts = fold update_const consts2 consts1,
       prmodes = insert (op =) mode prmodes,
       parse_ast_trtab =
@@ -489,7 +484,7 @@
     Syntax
     ({input = input',
       lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon,
-      gram = if changed then Future.value (Parser.extend_gram input' Parser.empty_gram) else gram,
+      gram = if changed then Lazy.value (Parser.make_gram input') else gram,
       consts = consts,
       prmodes = prmodes,
       parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
@@ -502,9 +497,9 @@
   end;
 
 
-(* merge_syntaxes *)
+(* merge_syntax *)
 
-fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) =
+fun merge_syntax (Syntax (tabs1, _), Syntax (tabs2, _)) =
   let
     val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1,
       prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
@@ -515,12 +510,22 @@
       prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
       parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2,
       print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2;
+
+    val (input', gram') =
+      (case subtract (op =) input1 input2 of
+        [] => (input1, gram1)
+      | new_xprods2 =>
+          if subset (op =) (input1, input2) then (input2, gram2)
+          else
+            let
+              val input' = new_xprods2 @ input1;
+              val gram' = Lazy.lazy (fn () => Parser.make_gram input');
+            in (input', gram') end);
   in
     Syntax
-    ({input = Library.merge (op =) (input1, input2),
+    ({input = input',
       lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
-      gram = future_gram [gram1, gram2] (fn () =>
-        Parser.merge_gram (Future.join gram1, Future.join gram2)),
+      gram = gram',
       consts = Symtab.merge (K true) (consts1, consts2),
       prmodes = Library.merge (op =) (prmodes1, prmodes2),
       parse_ast_trtab =
@@ -560,7 +565,7 @@
     val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
   in
     [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
-      Pretty.big_list "prods:" (Parser.pretty_gram (Future.join gram)),
+      Pretty.big_list "prods:" (Parser.pretty_gram (Lazy.force gram)),
       pretty_strs_qs "print modes:" prmodes']
   end;
 
@@ -596,7 +601,7 @@
 (* reconstructing infixes -- educated guessing *)
 
 fun guess_infix (Syntax ({gram, ...}, _)) c =
-  (case Parser.guess_infix_lr (Future.join gram) c of
+  (case Parser.guess_infix_lr (Lazy.force gram) c of
     SOME (s, l, r, j) => SOME
      (if l then Mixfix.Infixl (s, j)
       else if r then Mixfix.Infixr (s, j)

--- a/src/Pure/sign.ML	Fri Nov 25 14:23:36 2011 +0100
+++ b/src/Pure/sign.ML	Fri Nov 25 16:32:29 2011 +0100
@@ -149,7 +149,7 @@
       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
 
       val naming = Name_Space.default_naming;
-      val syn = Syntax.merge_syntaxes syn1 syn2;
+      val syn = Syntax.merge_syntax (syn1, syn2);
       val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
     in make_sign (naming, syn, tsig, consts) end;

--- a/src/Pure/theory.ML	Fri Nov 25 14:23:36 2011 +0100
+++ b/src/Pure/theory.ML	Fri Nov 25 16:32:29 2011 +0100
@@ -147,7 +147,7 @@
     |> Sign.local_path
     |> Sign.map_naming (Name_Space.set_theory_name name)
     |> apply_wrappers wrappers
-    |> tap (Syntax.join_syntax o Sign.syn_of)
+    |> tap (Syntax.force_syntax o Sign.syn_of)
   end;
 
 fun end_theory thy =