src/Provers/quasi.ML
 changeset 15570 8d8c70b41bab parent 15531 08c8dad8e399 child 19250 932a50e2332f
1.1 --- a/src/Provers/quasi.ML	Thu Mar 03 09:22:35 2005 +0100
1.2 +++ b/src/Provers/quasi.ML	Thu Mar 03 12:43:01 2005 +0100
1.3 @@ -92,7 +92,7 @@
1.4    (* Internal exception, raised if contradiction ( x < x ) was derived *)
1.6  fun prove asms =
1.7 -  let fun pr (Asm i) = nth_elem (i, asms)
1.8 +  let fun pr (Asm i) = List.nth (asms, i)
1.9    |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
1.10    in pr end;
1.12 @@ -560,7 +560,7 @@
1.13    val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
1.14    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
1.15    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
1.16 -  val lesss = flat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
1.17 +  val lesss = List.concat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
1.18    val prfs = solveLeTrans  sign (lesss, C);
1.20    val (subgoal, prf) = mkconcl_trans  sign C;
1.21 @@ -581,7 +581,7 @@
1.22    val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
1.23    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
1.24    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
1.25 -  val lesss = flat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
1.26 +  val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
1.27    val prfs = solveQuasiOrder sign (lesss, C);
1.28    val (subgoals, prf) = mkconcl_quasi sign C;
1.29   in