src/HOL/Tools/inductive_codegen.ML

              let
                val (args1, args2) = chop (length ms) args;
                val (gr', (ps, mode_id)) = foldl_map
                    (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
                  modename module name mode;
-               val (gr'', ps') = foldl_map
-                 (invoke_codegen thy defs dep module true) (gr', args2)
+               val (gr'', ps') = (case mode of
+                   ([], []) => (gr', [Pretty.str "()"])
+                 | _ => foldl_map
+                     (invoke_codegen thy defs dep module true) (gr', args2))
              in (gr', (if brack andalso not (null ps andalso null ps') then
                single o parens o Pretty.block else I)
                  (List.concat (separate [Pretty.brk 1]
                    ([Pretty.str mode_id] :: ps @ map single ps'))))
              end

                  let
                    val (in_ts, out_ts''') = get_args js 1 us;
                    val (gr2, in_ps) = foldl_map
                      (invoke_codegen thy defs dep module true) (gr1, in_ts);
                    val (gr3, ps) = if is_ind t then
-                       apsnd (fn ps => ps @ Pretty.brk 1 ::
+                       apsnd (fn ps => ps @
+                           (if null in_ps then [] else [Pretty.brk 1]) @
                            separate (Pretty.brk 1) in_ps)
                          (compile_expr thy defs dep module false modes
                            (gr2, (mode, t)))
                      else
                        apsnd (fn p => [Pretty.str "Seq.of_list", Pretty.brk 1, p])

       modename module s mode
   in
     ((gr', "and "), Pretty.block
       ([Pretty.block (separate (Pretty.brk 1)
          (Pretty.str (prfx ^ mode_id) ::
-           map Pretty.str arg_vs @ xs) @
+           map Pretty.str arg_vs @
+           (case mode of ([], []) => [Pretty.str "()"] | _ => xs)) @
          [Pretty.str " ="]),
         Pretty.brk 1] @
        List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
   end;
 

           mk_ind_def thy defs gr dep names (if_library thyname module)
             [] (prep_intrs intrs) nparms))
             (gr, foldr add_term_consts [] ts)
 
 and mk_ind_def thy defs gr dep names module modecs intrs nparms =
-  add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
+  add_edge_acyclic (hd names, dep) gr handle
+    Graph.CYCLES (xs :: _) =>
+      error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs)
+  | Graph.UNDEF _ =>
     let
       val _ $ u = Logic.strip_imp_concl (hd intrs);
       val args = List.take (snd (strip_comb u), nparms);
       val arg_vs = List.concat (map term_vs args);