1.1 --- a/src/Tools/isac/Specify/refine.sml	Mon Nov 07 19:49:14 2022 +0100
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Mon Nov 07 19:58:01 2022 +0100
     1.3 @@ -5,8 +5,8 @@
     1.4  Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close> 
     1.5  better fitting the respective where_-condition.
     1.6  
     1.7 -The search on the tree got by @{term KEStore_Elems.get_pbls} is costly such that 
     1.8 -\<open>ML_structure KEStore_Elems\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, where_-condition (and cas).
     1.9 +The search on the tree got by @{term Know_Store.get_pbls} is costly such that 
    1.10 +\<open>ML_structure Know_Store\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, where_-condition (and cas).
    1.11  The terms are where_-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
    1.12  according to the type suggested by the current \<open>ML_structure Context\<close>.
    1.13