explicit join_syntax ensures command transaction integrity of 'theory';

--- a/src/Pure/Syntax/syntax.ML	Wed Sep 07 20:49:45 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Sep 07 21:05:53 2011 +0200
@@ -99,6 +99,7 @@
   val string_of_sort_global: theory -> sort -> string
   type syntax
   val eq_syntax: syntax * syntax -> bool
+  val join_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
@@ -508,6 +509,8 @@
 
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
 
+fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join 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;

--- a/src/Pure/theory.ML	Wed Sep 07 20:49:45 2011 +0200
+++ b/src/Pure/theory.ML	Wed Sep 07 21:05:53 2011 +0200
@@ -147,6 +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)
   end;
 
 fun end_theory thy =