1.1 --- a/src/Tools/isac/Interpret/solve.sml	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -143,7 +143,7 @@
     1.4     val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
     1.5     *)
     1.6  fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
     1.7 -      let val {srls, ...} = get_met mI;
     1.8 +      let val {srls, ...} = Specify.get_met mI;
     1.9          val PblObj {meth=itms, ...} = get_obj I pt p;
    1.10          val thy' = get_obj g_domID pt p;
    1.11          val thy = assoc_thy thy';
    1.12 @@ -192,7 +192,7 @@
    1.13  		       | _ => get_assumptions_ pt (p,p_))
    1.14  	        handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    1.15          val metID = get_obj g_metID pt pp;
    1.16 -        val {srls=srls,scr=sc,...} = get_met metID;
    1.17 +        val {srls=srls,scr=sc,...} = Specify.get_met metID;
    1.18          val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
    1.19          val thy' = get_obj g_domID pt pp;
    1.20          val thy = assoc_thy thy';
    1.21 @@ -211,7 +211,7 @@
    1.22  	          val thy' = get_obj g_domID pt ppp;
    1.23              val thy = assoc_thy thy';
    1.24  	          val metID = get_obj g_metID pt ppp;
    1.25 -            val sc = (#scr o get_met) metID;
    1.26 +            val sc = (#scr o Specify.get_met) metID;
    1.27              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 
    1.28  	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
    1.29              val ((p,p_),ps,f,pt) = 
    1.30 @@ -274,7 +274,7 @@
    1.31  (* nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)
    1.32  fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
    1.33        let
    1.34 -        val {srls,ppc,...} = get_met mI;
    1.35 +        val {srls,ppc,...} = Specify.get_met mI;
    1.36          val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
    1.37          val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
    1.38          val thy' = get_obj g_domID pt p;
    1.39 @@ -311,7 +311,7 @@
    1.40  		       | _ => get_assumptions_ pt (p,p_))
    1.41  	        handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
    1.42          val metID = get_obj g_metID pt pp;
    1.43 -        val {srls=srls,scr=sc,...} = get_met metID;
    1.44 +        val {srls=srls,scr=sc,...} = Specify.get_met metID;
    1.45          val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
    1.46          val thy' = get_obj g_domID pt pp;
    1.47          val thy = assoc_thy thy';
    1.48 @@ -331,7 +331,7 @@
    1.49  	          val thy' = get_obj g_domID pt ppp;
    1.50              val thy = assoc_thy thy';
    1.51  	          val metID = get_obj g_metID pt ppp;
    1.52 -	          val {scr,...} = get_met metID;
    1.53 +	          val {scr,...} = Specify.get_met metID;
    1.54              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
    1.55  	          val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
    1.56              val tac_ = Check_Postcond' (pI, (scval, asm))