1.1 --- a/src/Tools/isac/Specify/refine.sml	Thu Sep 15 10:07:12 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Fri Sep 16 12:13:23 2022 +0200
     1.3 @@ -2,7 +2,16 @@
     1.4     Author: Walther Neuper 110226
     1.5     (c) due to copyright terms
     1.6  
     1.7 -Operations on models.
     1.8 +Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close> 
     1.9 +better fitting the respective pre-condition.
    1.10 +
    1.11 +The search on the tree got by @{term KEStore_Elems.get_pbls} is costly such that 
    1.12 +\<open>ML_structure KEStore_Elems\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, pre-condition (and cas).
    1.13 +The terms are pre-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
    1.14 +according to the type suggested by the current \<open>ML_structure Context\<close>.
    1.15 +
    1.16 +Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
    1.17 +are adapted for "adapt_to_type on the fly" until further clarification.
    1.18  *)
    1.19  
    1.20  signature REFINE_PROBLEM =