src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 42090 908dfde7cf75
parent 42023 927cb6806af1
child 42092 1a6d6089e594
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri Jul 15 10:17:51 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri Jul 15 13:51:50 2011 +0200
     1.3 @@ -411,12 +411,11 @@
     1.4      | (_, c', ptp') => complete_solve auto (c @ c') ptp'
     1.5  
     1.6  and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = 
     1.7 -   let
     1.8 -     val (_,_,mI) = get_obj g_spec pt p;
     1.9 -     val ctxt = get_ctxt pt pos
    1.10 -     val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
    1.11 -			 (e_istate, ctxt) ptp;
    1.12 -   in complete_solve auto (c @ c') ptp end;
    1.13 +  let
    1.14 +    val (_,_,mI) = get_obj g_spec pt p;
    1.15 +    val ctxt = get_ctxt pt pos
    1.16 +    val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
    1.17 +  in complete_solve auto (c @ c') ptp end;
    1.18  
    1.19  fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
    1.20    if p = ([], Res)
    1.21 @@ -452,8 +451,7 @@
    1.22    let
    1.23      val (_,_,mI) = get_obj g_spec pt p
    1.24      val ctxt = get_ctxt pt pos
    1.25 -    val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
    1.26 -			(e_istate, ctxt) ptp
    1.27 +    val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp
    1.28    in complete_solve auto (c @ c') ptp end;
    1.29  
    1.30  (* aux.fun for detailrls with Rrls, reverse rewriting *)