src/Provers/trancl.ML
 changeset 15570 8d8c70b41bab parent 15531 08c8dad8e399 child 15574 b1d1b5bfc464
```--- a/src/Provers/trancl.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Provers/trancl.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -88,7 +88,7 @@
exception Cannot; (* internal exception: raised if no proof can be found *)

fun prove asms =
-  let fun pr (Asm i) = nth_elem (i, asms)
+  let fun pr (Asm i) = List.nth (asms, i)
|       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
in pr end;

@@ -327,7 +327,7 @@

(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
-   val flipped = foldr (op @) ((map flip g),nil)
+   val flipped = Library.foldr (op @) ((map flip g),nil)

in assemble g flipped end

@@ -351,7 +351,7 @@
let
val _ = visited := u :: !visited
val descendents =
-       foldr (fn ((v,l),ds) => if been_visited v then ds
+       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
( ((adjacent eq_comp g u)) ,nil)
in  descendents end
@@ -530,7 +530,7 @@
val Hs = Logic.strip_assums_hyp A;
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 = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
val prfs = solveTrancl (prems, C);

in
@@ -548,7 +548,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 = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
val prfs = solveRtrancl (prems, C);
in
METAHYPS (fn asms =>```