src/HOL/Tools/inductive_codegen.ML

         val (nvs', t') = distinct_v (nvs, t);
         val (nvs'', u') = distinct_v (nvs', u);
       in (nvs'', t' $ u') end
   | distinct_v x = x;
 
-fun compile_match nvs eq_ps out_ps success_p fail_p =
+fun is_exhaustive (Var _) = true
+  | is_exhaustive (Const ("Pair", _) $ t $ u) =
+      is_exhaustive t andalso is_exhaustive u
+  | is_exhaustive _ = false;
+
+fun compile_match nvs eq_ps out_ps success_p can_fail =
   let val eqs = flat (separate [Pretty.str " andalso", Pretty.brk 1]
     (map single (flat (map (mk_eq o snd) nvs) @ eq_ps)));
   in
     Pretty.block
      ([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @
       (Pretty.block ((if eqs=[] then [] else Pretty.str "if " ::
          [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @
          (success_p ::
-          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else ", fail_p]))) ::
-       [Pretty.brk 1, Pretty.str "| _ => ", fail_p, Pretty.str ")"]))
+          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else Seq.empty"]))) ::
+       (if can_fail then
+          [Pretty.brk 1, Pretty.str "| _ => Seq.empty)"]
+        else [Pretty.str ")"])))
   end;
 
 fun modename thy s (iss, is) = space_implode "__"
   (mk_const_id (sign_of thy) s ::
     map (space_implode "_" o map string_of_int) (mapfilter I iss @ [is]));

               (invoke_codegen thy dep false) (gr3, out_ts''');
             val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
           in
             (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
               (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
-              (Pretty.str "Seq.empty"))
+              (exists (not o is_exhaustive) out_ts'''))
           end
       | compile_prems out_ts vs names gr ps =
           let
             val vs' = distinct (flat (vs :: map term_vs out_ts));
             val Some (p, mode as Some (Mode ((_, js), _))) =

                    val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
                  in
                    (gr4, compile_match (snd nvs) eq_ps out_ps
                       (Pretty.block (ps @
                          [Pretty.str " :->", Pretty.brk 1, rest]))
-                      (Pretty.str "Seq.empty"))
+                      (exists (not o is_exhaustive) out_ts''))
                  end
              | Sidecond t =>
                  let
                    val (gr2, side_p) = invoke_codegen thy dep true (gr1, t);
                    val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
                  in
                    (gr3, compile_match (snd nvs) eq_ps out_ps
                       (Pretty.block [Pretty.str "?? ", side_p,
                         Pretty.str " :->", Pretty.brk 1, rest])
-                      (Pretty.str "Seq.empty"))
+                      (exists (not o is_exhaustive) out_ts''))
                  end)
           end;
 
     val (gr', prem_p) = compile_prems in_ts' [] all_vs' gr ps;
   in