Removed Logic.skip_flexpairs.
authorberghofe
Mon, 21 Oct 2002 17:17:40 +0200
changeset 13668 11397ea8b438
parent 13667 0009325e9af0
child 13669 a9f229eafba7
Removed Logic.skip_flexpairs.
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;