src/Tools/isac/Interpret/mstools.sml
branchdecompose-isar
changeset 42009 5f5807893ceb
parent 41990 99e83a0bea44
child 42019 3e70f56104a8
     1.1 --- a/src/Tools/isac/Interpret/mstools.sml	Wed May 18 16:06:00 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Thu May 19 19:28:22 2011 +0200
     1.3 @@ -960,12 +960,9 @@
     1.4  fun pre2str (b, t) = pair2str(bool2str b, term2str t);
     1.5  fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
     1.6  
     1.7 -(*. check preconditions, return true if all true .*)
     1.8 +(* check preconditions, return true if all true *)
     1.9  fun check_preconds' _ [] _ _ = []  (*empty preconditions are true*)
    1.10    | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =
    1.11 -(* val (prls, pres, pbl, _) = (prls, where_, probl, 0);
    1.12 -   val (prls, pres, pbl, _) = (prls, pre, itms, mvat);
    1.13 -   *)
    1.14      let val env = mk_env pbl;
    1.15          val pres' = map (subst_atomic_all env) pres;
    1.16      in map (evalprecond prls) pres' end;
    1.17 @@ -1012,6 +1009,7 @@
    1.18    fun insert_environments envs = map (fn t => Env t) envs |> insert_ctxt;
    1.19  end
    1.20  
    1.21 +(* transfer information set by Variable.declare_constraints *)
    1.22  fun transfer_from_subproblem ctxt_sub ctxt =
    1.23    insert_assumptions (get_assumptions ctxt_sub) ctxt;
    1.24