author traytel Mon, 10 Sep 2012 09:56:06 +0200 changeset 49240 f7e75b802ef2 parent 49239 fdac10715b6b child 49241 fd11fe9dc6bb
stabilized generation of parameterized theorem
```--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 10 06:46:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 10 09:56:06 2012 +0200
@@ -247,14 +247,11 @@
if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
in split limit 1 th end;

-local
-  fun mk_sumEN' 1 = @{thm obj_sum_step}
-    | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
-in
-  fun mk_sumEN 1 = @{thm obj_sum_base}
-    | mk_sumEN 2 = @{thm sumE}
-    | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
-end;
+fun mk_sumEN 1 = @{thm obj_sum_base}
+  | mk_sumEN 2 = @{thm sumE}
+  | mk_sumEN n =
+    (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
+      replicate n (impI RS allI);

fun mk_sum_casesN 1 1 = @{thm refl}
| mk_sum_casesN _ 1 = @{thm sum.cases(1)}```