src/Tools/isac/Specify/step-specify.sml
changeset 59984 08296690e7a6
parent 59983 f1fdb213717b
child 59986 ecf545b44428
     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)