1.1 --- a/src/Tools/isac/Specify/refine.sml	Thu Jan 26 19:02:41 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Sat Jan 28 13:21:39 2023 +0100
     1.3 @@ -5,10 +5,12 @@
     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 Know_Store.get_pbls} is costly such that 
     1.8 -\<open>ML_structure Know_Store\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, where_-condition (and cas).
     1.9 -The terms are where_-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
    1.10 -according to the type suggested by the current \<open>ML_structure Context\<close>.
    1.11 +The search on the tree given by @{term Know_Store.get_pbls} is costly such that 
    1.12 +\<open>ML_structure Know_Store\<close> holds terms pre-parsed with a most generally type. 
    1.13 +
    1.14 +On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type
    1.15 +(and users of this function in \<open>ML_structure Error_Pattern, MethodC, Problem\<close>)
    1.16 +according to the current context.
    1.17  
    1.18  Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
    1.19  are adapted for "adapt_to_type on the fly" until further clarification.