# HG changeset patch # User wenzelm # Date 963522674 -7200 # Node ID b5a29408dc39ad60d1904a8b5a30d88307e084b7 # Parent a93a7b6bb654b04429071b029d63b4bce5a88841 fixed simplified_cases; diff -r a93a7b6bb654 -r b5a29408dc39 src/HOL/Tools/induct_method.ML --- 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;