1.1 --- a/src/Tools/isac/Specify/refine.sml	Wed Jul 27 13:11:43 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Wed Jul 27 13:59:58 2022 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4    end;
     1.5  
     1.6  fun problem thy pblID itms =
     1.7 -  case refined_ ((Store.apply (get_ptyps ())) (refin'' thy ((rev o tl) pblID) itms [])
     1.8 +  case refined_ ((Store.apply (get_pbls ())) (refin'' thy ((rev o tl) pblID) itms [])
     1.9        pblID (rev pblID)) of
    1.10  	  NONE => NONE
    1.11    | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
    1.12 @@ -193,7 +193,7 @@
    1.13  \<close>
    1.14  
    1.15  (* apply a fun to a ptyps node *)
    1.16 -fun app_ptyp x = Store.apply (get_ptyps ()) x;
    1.17 +fun app_ptyp x = Store.apply (get_pbls ()) x;
    1.18  
    1.19  (* for tactic Refine_Tacitly
    1.20     oris are already created wrt. some pbt; pbt contains thy for parsing *)