src/HOL/Tools/inductive_codegen.ML

   end;
 
 (**** theory data ****)
 
 fun merge_rules tabs =
-  Symtab.join (fn _ => fn (ths, ths') =>
-    gen_merge_lists (Thm.eq_thm_prop o pairself fst) ths ths') tabs;
+  Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
 
 structure CodegenData = TheoryDataFun
 (struct
   val name = "HOL/inductive_codegen";
   type T =

       NONE => thyname_of_const s thy | SOME s => s);
   in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
       SOME (Const ("op =", _), [t, _]) => (case head_of t of
         Const (s, _) =>
           CodegenData.put {intros = intros, graph = graph,
-             eqns = eqns |> Symtab.update
-               (s, Symtab.lookup_list eqns s @ [(thm, thyname_of s)])} thy
+             eqns = eqns |> Symtab.map_default (s, [])
+               (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
       | _ => (warn thm; thy))
     | SOME (Const (s, _), _) =>
         let
           val cs = foldr add_term_consts [] (prems_of thm);
           val rules = Symtab.lookup_list intros s;

                  SOME (_, {raw_induct, ...}) => length (params_of raw_induct)
                | NONE => 0)
             | xs => snd (snd (snd (split_last xs)))))
         in CodegenData.put
           {intros = intros |>
-           Symtab.update (s, rules @ [(thm, (thyname_of s, nparms))]),
+           Symtab.update (s, (AList.update Thm.eq_thm_prop
+             (thm, (thyname_of s, nparms)) rules)),
            graph = foldr (uncurry (Graph.add_edge o pair s))
              (Library.foldl add_node (graph, s :: cs)) cs,
            eqns = eqns} thy
         end
     | _ => (warn thm; thy))

   in case Symtab.lookup intros s of
       NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
         NONE => NONE
       | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
           SOME (names, thyname_of_const s thy, length (params_of raw_induct),
-            preprocess thy intrs))
+            preprocess thy (rev intrs)))
     | SOME _ =>
         let
           val SOME names = find_first
-            (fn xs => s mem xs) (Graph.strong_conn graph);
-          val intrs = List.concat (map
-            (fn s => the (Symtab.lookup intros s)) names);
-          val (_, (_, (thyname, nparms))) = split_last intrs
-        in SOME (names, thyname, nparms, preprocess thy (map fst intrs)) end
+            (fn xs => member (op =) xs s) (Graph.strong_conn graph);
+          val intrs as (_, (thyname, nparms)) :: _ =
+            maps (the o Symtab.lookup intros) names;
+        in SOME (names, thyname, nparms, preprocess thy (map fst (rev intrs))) end
   end;
 
 
 (**** check if a term contains only constructor functions ****)
 

       ~1 => true
     | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
       p ^ " violates mode " ^ string_of_mode m); false)) ms)
   end;
 
-fun fixp f x =
+fun fixp f (x : (string * (int list option list * int list) list) list) =
   let val y = f x
   in if x = y then x else fixp f y end;
 
 fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
   map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)

         (ks @ [SOME k]))) arities));
 
 fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
 
 fun constrain cs [] = []
-  | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs s of
+  | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
       NONE => xs
     | SOME xs' => xs inter xs') :: constrain cs ys;
 
 fun mk_extra_defs thy defs gr dep names module ts =
   Library.foldl (fn (gr, name) =>

              end handle TERM _ => mk_ind_call thy defs gr dep module true
                s T ts names thyname k intrs)
       | _ => NONE)
     | SOME eqns =>
         let
-          val (_, (_, thyname)) = split_last eqns;
-          val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
+          val (_, thyname) :: _ = eqns;
+          val (gr', id) = mk_fun thy defs s (preprocess thy (map fst (rev eqns)))
             dep module (if_library thyname module) gr;
           val (gr'', ps) = foldl_map
             (invoke_codegen thy defs dep module true) (gr', ts);
         in SOME (gr'', mk_app brack (Pretty.str id) ps)
         end)