# HG changeset patch
# User blanchet
# Date 1425570324 -3600
# Node ID 7ea413656b64f07ae136bb4a7cf70f28406b4e92
# Parent  63f8527db07fdc53f4fb1057391c40d60f0e5514
avoid needless 'if ... undefined' in generated theorems

diff -r 63f8527db07f -r 7ea413656b64 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 15:44:37 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Mar 05 16:45:24 2015 +0100
@@ -240,9 +240,11 @@
         (case Term.strip_comb t of
           (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
         | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
-          let val branches' = map (massage_rec bound_Ts) branches in
-            Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
-          end
+          (case List.partition Term.is_dummy_pattern (map (massage_rec bound_Ts) branches) of
+            (dummy_branch' :: _, []) => dummy_branch'
+          | (_, [branch']) => branch'
+          | (_, branches') =>
+            Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches'))
         | (c as Const (@{const_name case_prod}, _), arg :: args) =>
           massage_rec bound_Ts
             (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
@@ -278,6 +280,8 @@
       end;
   in
     massage_rec bound_Ts t0
+    |> Term.map_aterms (fn t =>
+      if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t)
   end;
 
 fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
@@ -771,7 +775,7 @@
     val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
       binder_types (fastype_of ctr)
       |> map_index (fn (n, T) => massage_corec_code_rhs ctxt (fn _ => fn ctr' => fn args =>
-        if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
+        if ctr' = ctr then nth args n else Term.dummy_pattern T) [] rhs')
       |> curry Term.list_comb ctr
       |> curry HOLogic.mk_eq lhs);