--- a/src/Provers/trancl.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/Provers/trancl.ML Thu Oct 22 13:48:06 2009 +0200
@@ -538,7 +538,7 @@
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_trancl C;
- val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
+ val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
val prfs = solveTrancl (prems, C);
in
Subgoal.FOCUS (fn {prems, ...} =>
@@ -555,7 +555,7 @@
val C = Logic.strip_assums_concl A;
val (rel, subgoals, prf) = mkconcl_rtrancl C;
- val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
+ val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
val prfs = solveRtrancl (prems, C);
in
Subgoal.FOCUS (fn {prems, ...} =>