src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 42014 2863ed75b595
parent 42006 8749a1abdbd2
child 42018 11cf93cd02c6
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri May 20 08:20:53 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri May 20 08:32:57 2011 +0200
     1.3 @@ -144,10 +144,10 @@
     1.4     *)
     1.5  fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
     1.6        let val {srls, ...} = get_met mI;
     1.7 -        val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
     1.8 +        val PblObj {meth=itms, ...} = get_obj I pt p;
     1.9          val thy' = get_obj g_domID pt p;
    1.10          val thy = assoc_thy thy';
    1.11 -        val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
    1.12 +        val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
    1.13          val ini = init_form thy sc env;
    1.14          val p = lev_dn p;
    1.15        in 
    1.16 @@ -274,11 +274,11 @@
    1.17  fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
    1.18        let
    1.19          val {srls,ppc,...} = get_met mI;
    1.20 -        val PblObj{meth=itms,origin=(oris,_,_),probl, ctxt, ...} = get_obj I pt p;
    1.21 +        val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
    1.22          val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
    1.23          val thy' = get_obj g_domID pt p;
    1.24          val thy = assoc_thy thy';
    1.25 -        val (is as ScrState (env,_,_,_,_,_), _, scr) = init_scrstate thy itms mI;
    1.26 +        val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
    1.27          val ini = init_form thy scr env;
    1.28        in 
    1.29          case ini of