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 -------------------------------------------------------*)