src/Tools/coherent.ML
changeset 31855 7c2a5e79a654
parent 31241 b3c7044d47b6
child 32035 8e77b6a250d5
     1.1 --- a/src/Tools/coherent.ML	Mon Jun 29 14:55:08 2009 +0200
     1.2 +++ b/src/Tools/coherent.ML	Mon Jun 29 20:05:44 2009 +0200
     1.3 @@ -110,9 +110,9 @@
     1.4  (* Check whether disjunction is valid in given state *)
     1.5  fun is_valid_disj ctxt facts [] = false
     1.6    | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
     1.7 -      let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts)
     1.8 +      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts
     1.9        in case Seq.pull (valid_conj ctxt facts empty_env
    1.10 -        (map (fn t => subst_bounds (vs, t)) ts)) of
    1.11 +        (map (fn t => subst_bounds (rev vs, t)) ts)) of
    1.12            SOME _ => true
    1.13          | NONE => is_valid_disj ctxt facts ds
    1.14        end;
    1.15 @@ -153,10 +153,10 @@
    1.16    | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
    1.17        let
    1.18          val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
    1.19 -        val params = rev (map_index (fn (i, T) =>
    1.20 -          Free ("par" ^ string_of_int (nparams + i), T)) Ts);
    1.21 +        val params = map_index (fn (i, T) =>
    1.22 +          Free ("par" ^ string_of_int (nparams + i), T)) Ts;
    1.23          val ts' = map_index (fn (i, t) =>
    1.24 -          (subst_bounds (params, t), nfacts + i)) ts;
    1.25 +          (subst_bounds (rev params, t), nfacts + i)) ts;
    1.26          val dom' = fold (fn (T, p) =>
    1.27            Typtab.map_default (T, []) (fn ps => ps @ [p]))
    1.28              (Ts ~~ params) dom;