1.1 --- a/src/Tools/isac/Specify/step-specify.sml Fri May 15 11:46:43 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/step-specify.sml Fri May 15 14:22:05 2020 +0200
1.3 @@ -132,7 +132,7 @@
1.4 val pbl =
1.5 if pI' = Problem.id_empty andalso pI = Problem.id_empty
1.6 then (false, (I_Model.init ppc, []))
1.7 - else Model.match_itms_oris thy probl (ppc,where_,prls) oris
1.8 + else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris
1.9 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.10 val (c, pt) =
1.11 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
1.12 @@ -153,7 +153,7 @@
1.13 val thy = ThyC.get_theory dI
1.14 val oris = O_Model.add thy ppc oris
1.15 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1.16 - val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris
1.17 + val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc,pre,prls ) oris
1.18 val itms = hack_until_review_Specify_2 mID itms
1.19 val (pos, c, _, pt) =
1.20 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
1.21 @@ -249,7 +249,7 @@
1.22 val thy = ThyC.get_theory dI
1.23 val oris = O_Model.add thy ppc oris
1.24 val met = if met = [] then pbl else met
1.25 - val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris
1.26 + val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc, pre, prls) oris
1.27 val itms = hack_until_review_Specify_1 mI' itms
1.28 val (pos, _, _, pt) =
1.29 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)