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