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.5  
     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.11  
    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.19    
    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