134 (tac_2tac tac_, tac_, (p, get_istate pt p)):taci; |
134 (tac_2tac tac_, tac_, (p, get_istate pt p)):taci; |
135 |
135 |
136 |
136 |
137 |
137 |
138 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); |
138 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); |
139 val (("Apply_Method",Apply_Method' (mI,_)), pos as (p,_))=(m, pos); |
139 val (("Apply_Method",Apply_Method' (mI,_,_)), pos as (p,_))=(m, pos); |
140 *) |
140 *) |
141 fun solve ("Apply_Method",Apply_Method' (mI,_,_)) (pt:ptree,(pos as (p,_))) = |
141 fun solve ("Apply_Method",Apply_Method' (mI,_,_)) (pt:ptree,(pos as (p,_))) = |
142 let val {srls,...} = get_met mI; |
142 let val {srls,...} = get_met mI; |
143 val PblObj{meth=itms,...} = get_obj I pt p; |
143 val PblObj{meth=itms,...} = get_obj I pt p; |
144 val thy' = get_obj g_domID pt p; |
144 val thy' = get_obj g_domID pt p; |