tuned
authorwneuper <Walther.Neuper@jku.at>
Wed, 27 Jul 2022 14:04:04 +0200
changeset 604965fb1fa7aad13
parent 60495 54642eaf7bba
child 60497 cd067c85c311
tuned
TODO.md
test/Tools/isac/Specify/refine.sml
     1.1 --- a/TODO.md	Wed Jul 27 13:59:58 2022 +0200
     1.2 +++ b/TODO.md	Wed Jul 27 14:04:04 2022 +0200
     1.3 @@ -99,8 +99,6 @@
     1.4  
     1.5  * WN: rename in Formalise: type spec = Model_Def.form_spec;
     1.6                             type refs = Model_Def.form_refs;
     1.7 -* WN: rename in Know_Store: get_ptyps, add_pbls
     1.8 -                            get_pbls,  add_pbls
     1.9  * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
    1.10    - init_ctree, update_status, check_input
    1.11  
     2.1 --- a/test/Tools/isac/Specify/refine.sml	Wed Jul 27 13:59:58 2022 +0200
     2.2 +++ b/test/Tools/isac/Specify/refine.sml	Wed Jul 27 14:04:04 2022 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4  "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
     2.5  "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
     2.6  (* fragile test setup: expects ptyps as fixed *)
     2.7 -val level_1 = case nth 9 (get_ptyps ()) of
     2.8 +val level_1 = case nth 9 (get_pbls ()) of
     2.9  Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
    2.10  val level_2 = case nth 4 level_1 of
    2.11  Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
    2.12 @@ -447,7 +447,7 @@
    2.13  "~~~~~ fun problem , args:"; val (thy, pblID, itms) = ((ThyC.get_theory thy), pI, probl);
    2.14  (*  val SOME (Refine.Match_ (["sqroot-test", "univariate", "equation", "test"], _)) =*)
    2.15    val SOME (Refine.Match_ (rfd as (pI', _))) = (*case*) 
    2.16 -    Refine.refined_ ((Store.apply (get_ptyps ())) (Refine.refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) (*of*);
    2.17 +    Refine.refined_ ((Store.apply (get_pbls ())) (Refine.refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) (*of*);
    2.18      (*if*) pblID = pI' (*then*);
    2.19      NONE  (*return from problem*);
    2.20  (*-------------------- stop step into -------------------------------------------------------*)