src/Tools/isac/Specify/step-specify.sml
changeset 59971 2909d58a5c5d
parent 59970 ab1c25c0339a
child 59975 c4b83a338c44
     1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Tue May 12 17:42:29 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Wed May 13 11:34:05 2020 +0200
     1.3 @@ -97,7 +97,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 Specify.match_itms_oris thy probl (ppc,where_,prls) oris
     1.8 +	      else Model.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 @@ -118,7 +118,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, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
    1.17 +      val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris
    1.18        val itms = Specify.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 @@ -214,7 +214,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, _)) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
    1.26 +        val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris
    1.27          val itms = Specify.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)