# HG changeset patch
# User haftmann
# Date 1184570942 -7200
# Node ID 6104514a1f5f74a915ef81428a3af7be8188ca96
# Parent  4e4b92e76219b3260b0d9b47208d10191b4f3816
tuned

diff -r 4e4b92e76219 -r 6104514a1f5f src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Mon Jul 16 09:29:01 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Mon Jul 16 09:29:02 2007 +0200
@@ -291,8 +291,8 @@
           map (apfst (Thm.capply ct1)) (find_vars ct2)
         end
       | _ => []);
-    val eqs = List.concat (map
-      (fn th => map (pair th) (find_vars (lhs_of th))) thms);
+    val eqs = maps
+      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
     fun mk_thms (th, (ct, cv')) =
       let
         val th' =
diff -r 4e4b92e76219 -r 6104514a1f5f src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Jul 16 09:29:01 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Jul 16 09:29:02 2007 +0200
@@ -991,7 +991,8 @@
           add_group mk_class defs
       | group_defs ((defs as [(_, CodegenThingol.Classinst _)])) =
           add_group mk_inst defs
-      | group_defs defs = error ("Illegal mutual dependencies: " ^ (commas o map (labelled_name o fst)) defs)
+      | group_defs defs = error ("Illegal mutual dependencies: " ^
+          (commas o map (labelled_name o fst)) defs)
     val (_, nodes) =
       init_module
       |> fold group_defs (map (AList.make (Graph.get_node code))
@@ -1016,15 +1017,13 @@
     fun pr_node prefix (Def (_, NONE)) =
           NONE
       | pr_node prefix (Def (_, SOME def)) =
-          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms (deresolver prefix) is_cons def)
+          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
+            (deresolver prefix) is_cons def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
           SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
             @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
                 o rev o flat o Graph.strong_conn) nodes)));
-    val mk_frame = if is_some module
-      then Pretty.chunks
-      else pr_modl "ROOT"
-    val p = mk_frame (the_prolog "" @ separate (str "") ((map_filter
+    val p = Pretty.chunks (the_prolog "" @ separate (str "") ((map_filter
       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
   in output p end;
 
@@ -1489,8 +1488,8 @@
 fun merge_syntax_modl (SyntaxModl { alias = alias1, prolog = prolog1 },
     SyntaxModl { alias = alias2, prolog = prolog2 }) =
   mk_syntax_modl (
-    Symtab.merge (K true) (alias1, alias2),
-    Symtab.merge (op =) (prolog1, prolog2)
+    Symtab.join (K snd) (alias1, alias2),
+    Symtab.join (K snd) (prolog1, prolog2)
   );
 
 type serializer =