--- a/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML Thu Oct 22 13:48:06 2009 +0200
@@ -363,7 +363,7 @@
val ineqss = mk_ineqs R scheme
|> map (map (pairself (assume o cert)))
- val complete = map (mk_completeness ctxt scheme #> cert #> assume) (0 upto (length branches - 1))
+ val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
val wf_thm = mk_wf ctxt R scheme |> cert |> assume
val (descent, pres) = split_list (flat ineqss)