# HG changeset patch
# User berghofe
# Date 1035213460 -7200
# Node ID 11397ea8b4388b7dae318e31255f659670763708
# Parent  0009325e9af013869eb9c4128b159380ea35138a
Removed Logic.skip_flexpairs.

diff -r 0009325e9af0 -r 11397ea8b438 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Mon Oct 21 17:16:24 2002 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Mon Oct 21 17:17:40 2002 +0200
@@ -98,7 +98,7 @@
 val empty = {fixes = [], assumes = [], binds = []};
 
 fun nth_subgoal(i,prop) =
-  hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop)));
+  hd (#1 (Logic.strip_prems (i, [], prop)));
 
 fun hhf_nth_subgoal sg = Drule.norm_hhf sg o nth_subgoal
   
@@ -128,7 +128,7 @@
   in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
 
 fun make open_params split (sg, prop) names =
-  let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in
+  let val nprems = Logic.count_prems (prop, 0) in
     foldr (fn (name, (cases, i)) => (prep_case open_params split sg prop name i :: cases, i - 1))
       (Library.drop (length names - nprems, names), ([], length names)) |> #1
   end;