--- a/src/HOL/Tools/induct_method.ML Thu Jul 13 23:10:12 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML Thu Jul 13 23:11:14 2000 +0200
@@ -206,8 +206,8 @@
val tac = simp_case_tac true (Simplifier.get_local_simpset ctxt);
fun simp ((i, c), (th, cs)) =
(case try (Tactic.rule_by_tactic (tac i)) th of
- None => (th, None :: cs)
- | Some th' => (th', c :: cs));
+ None => (th, c :: cs)
+ | Some th' => (th', None :: cs));
val (thm', opt_cases') = foldr simp (1 upto Thm.nprems_of thm ~~ opt_cases, (thm, []));
in (thm', mapfilter I opt_cases') end;