--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 09 19:10:35 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 09:48:11 2014 +0100
@@ -865,7 +865,7 @@
auto_gen = true,
ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
- eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 1000 (*###*),
+ eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (*###*),
user_eqn = undef_const};
in
chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
@@ -1235,7 +1235,8 @@
val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
val sel_thmss = map (map snd o order_list_duplicates) sel_alists;
- fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss' disc_thms
+ fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
+ (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
if null disc_thms orelse null exhaust_thms then
[]
@@ -1250,7 +1251,7 @@
if prems = [@{term False}] then
[]
else
- mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) fun_args)
+ mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
(the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
@@ -1258,8 +1259,8 @@
|> single
end;
- val disc_iff_thmss = map5 (flat ooo map2 ooo prove_disc_iff) corec_specs exhaust_thmss
- disc_thmsss' disc_thmsss' disc_eqnss
+ val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
+ disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
|> map order_list_duplicates;
val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists) disc_eqnss