# HG changeset patch # User blanchet # Date 1388652622 -3600 # Node ID 5d965f17b0e4233718b5405edc5a5ad867b116a4 # Parent c664bd02bf9403f222ac0d2fbe9233de25880f68 detect syntactic exhaustiveness diff -r c664bd02bf94 -r 5d965f17b0e4 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100 @@ -937,8 +937,8 @@ disc_eqnss; val nchotomy_goalss = - map2 (fn false => K [] - | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems) exhaustives disc_eqnss + map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems) + de_facto_exhaustives disc_eqnss |> list_all_fun_args val nchotomy_taut_thmss = (case maybe_tac of @@ -963,7 +963,7 @@ val exhaust_thmss = map2 (fn false => K [] | true => single o mk_imp_p o map (mk_imp_p o map HOLogic.mk_Trueprop o #prems)) - exhaustives disc_eqnss + de_facto_exhaustives disc_eqnss |> list_all_fun_args |> map3 (fn disc_eqns => fn [] => K [] | [nchotomy_thm] => fn [goal] =>