# HG changeset patch
# User wenzelm
# Date 1125506816 -7200
# Node ID ba65f3e5653c9e08a1730fb346d266a2f808b64a
# Parent  6859484b5b2bd79bd2fbec7d92c0cb74fc73dc22
fixed ins_tokentr: AList.default;

diff -r 6859484b5b2b -r ba65f3e5653c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Aug 31 17:53:35 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Aug 31 18:46:56 2005 +0200
@@ -120,8 +120,8 @@
 
     fun merge mode =
       let
-        val trs1 = (these o AList.lookup (op =) tabs1) mode;
-        val trs2 = (these o AList.lookup (op =) tabs2) mode;
+        val trs1 = these (AList.lookup (op =) tabs1 mode);
+        val trs2 = these (AList.lookup (op =) tabs2 mode);
         val trs = gen_distinct eq_tr (trs1 @ trs2);
       in
         (case gen_duplicates eq_fst trs of
@@ -135,8 +135,9 @@
 
 fun extend_tokentrtab tokentrs tabs =
   let
-    fun ins_tokentr (m, c, f) ts =
-      AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ()))) ts;
+    fun ins_tokentr (m, c, f) =
+      AList.default (op =) (m, [])
+      #> AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ())));
   in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;