src/Tools/isac/Specify/step-specify.sml
changeset 59960 d0637de46bfa
parent 59958 c06b7df89dcd
child 59962 6a59d252345d
     1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Sun May 10 17:26:36 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Mon May 11 11:07:19 2020 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4        | _ => error "by_tactic_input Refine_Problem: uncovered case get_obj"
     1.5  	    val thy = if dI' = ThyC.id_empty then dI else dI'
     1.6      in 
     1.7 -      case Specify.refine_pbl (ThyC.get_theory thy) pI probl of
     1.8 +      case Refine.problem (ThyC.get_theory thy) pI probl of
     1.9  	      NONE => ([], [], ptp)
    1.10  	    | SOME rfd => 
    1.11  	      let 
    1.12 @@ -116,7 +116,7 @@
    1.13        | _ => error "by_tactic_input Specify_Method: uncovered case get_obj"
    1.14        val {ppc,pre,prls,...} = Specify.get_met mID
    1.15        val thy = ThyC.get_theory dI
    1.16 -      val oris = Specify.add_field' thy ppc oris
    1.17 +      val oris = O_Model.add thy ppc oris
    1.18        val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
    1.19        val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
    1.20        val itms = Specify.hack_until_review_Specify_2 mID itms
    1.21 @@ -212,7 +212,7 @@
    1.22          | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
    1.23          val {ppc, pre, prls,...} = Specify.get_met mID
    1.24          val thy = ThyC.get_theory dI
    1.25 -        val oris = Specify.add_field' thy ppc oris
    1.26 +        val oris = O_Model.add thy ppc oris
    1.27          val met = if met = [] then pbl else met
    1.28          val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
    1.29          val itms = Specify.hack_until_review_Specify_1 mI' itms