1.1 --- a/src/Tools/isac/Specify/refine.sml	Wed Nov 09 15:15:24 2022 +0100
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Thu Nov 10 14:25:38 2022 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4  	  val itms'' = filter (okv mvat) itms';
     1.5  	  val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
     1.6  	  val mis = chk_mis mvat itms'' untouched pbt;
     1.7 -	  val (pb, where_')  = Pre_Conds.check where_rls where_ itms'' mvat
     1.8 +	  val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms'' mvat
     1.9    in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
    1.10  
    1.11  (* refine a problem; version for tactic Refine_Problem *)
    1.12 @@ -196,7 +196,7 @@
    1.13        val model = map (Model_Pattern.adapt_to_type ctxt) model
    1.14        val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
    1.15      in
    1.16 -      if M_Match.match_oris (Proof_Context.theory_of ctxt) where_rls ori (model, where_) 
    1.17 +      if M_Match.match_oris ctxt where_rls ori (model, where_) 
    1.18        then SOME (pblRD @ [pI])
    1.19        else NONE
    1.20      end
    1.21 @@ -206,7 +206,7 @@
    1.22        val model = map (Model_Pattern.adapt_to_type ctxt) model
    1.23        val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
    1.24      in
    1.25 -      if M_Match.match_oris (Proof_Context.theory_of ctxt) where_rls ori (model, where_) 
    1.26 +      if M_Match.match_oris ctxt where_rls ori (model, where_) 
    1.27        then (case refins ctxt (pblRD @ [pI]) ori pys of
    1.28  	        SOME pblRD' => SOME pblRD'
    1.29  	      | NONE => SOME (pblRD @ [pI]))