1.1 --- a/src/Tools/isac/Specify/refine.sml	Wed Nov 29 07:51:28 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Thu Nov 30 08:11:50 2023 +0100
     1.3 @@ -129,8 +129,10 @@
     1.4          val mid = max_id itms;
     1.5      in add_idvat [] (mid + 1) mvat mis end;
     1.6  
     1.7 -(* check a problem (ie. itm list) for matching a problemtype, 
     1.8 -   takes the Pre_Conds.max_variant for concluding completeness (could be another!) *)
     1.9 +(*
    1.10 +  check a problem (ie. i?model) for matching a problemtype, 
    1.11 +  takes the Pre_Conds.max_variant for concluding completeness
    1.12 +*)
    1.13  (*  match_itms: theory -> I_Model.T -> Model_Pattern.T * unchecked * Rule_Def.rule_set ->
    1.14           bool * (I_Model.T * (bool * term) list)*)
    1.15  fun match_itms thy itms (pbt, where_, where_rls) = 
    1.16 @@ -145,7 +147,7 @@
    1.17  	    (pbt, I_Model.OLD_to_TEST itms'')
    1.18    in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
    1.19  
    1.20 -(* refine a problem; version for tactic Refine_Problem *)
    1.21 +(* version for tactic Refine_Problem *)
    1.22  fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
    1.23      let
    1.24  	    val {thy, model, where_, where_rls, ...} = py
    1.25 @@ -262,12 +264,8 @@
    1.26        | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts
    1.27      end;
    1.28  
    1.29 -(*
    1.30 -  TODO: rename \<rightarrow> apply_to_node
    1.31 -  apply a fun to a ptyps node.
    1.32 -  val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
    1.33 -TODO: Store.apply scans Store.T only to the first hit; see Store.apply.
    1.34 -*)
    1.35 +(* Store.apply scans Store.T only to the first hit *)
    1.36 +(*val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a*)
    1.37  fun find_node_elem x = Store.apply (get_pbls ()) x;
    1.38  
    1.39  (*for tactic Refine_Tacitly; oris are already created wrt. some pbt; ctxt overrides thy in pbt*)