test/Tools/isac/Specify/refine.sml
changeset 60154 2ab0d1523731
parent 60021 d70d5b668794
child 60230 0ca0f9363ad3
     1.1 --- a/test/Tools/isac/Specify/refine.sml	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/test/Tools/isac/Specify/refine.sml	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -408,9 +408,9 @@
     1.4  "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
     1.5    (oris, (o_refs, refs), (pbl, met));
     1.6      val cpI = if pI = Problem.id_empty then pI' else pI;
     1.7 -    val cmI = if mI = Method.id_empty then mI' else mI;
     1.8 +    val cmI = if mI = MethodC.id_empty then mI' else mI;
     1.9      val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
    1.10 -    val {ppc = mpc, ...} = Method.from_store cmI
    1.11 +    val {ppc = mpc, ...} = MethodC.from_store cmI
    1.12      val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0;
    1.13      (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
    1.14        (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);