1.1 --- a/src/Tools/isac/Specify/sub-problem.sml	Sun Aug 27 16:48:03 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/sub-problem.sml	Sun Aug 27 17:47:56 2023 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    else if Context.subthy (thy2, thy1) then thy1
     1.5      else Know_Store.get_ref_last_thy ()
     1.6  
     1.7 -fun tac_from_prog (pt, p) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
     1.8 +fun tac_from_prog (pt, _) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
     1.9      let
    1.10        val (dI, pI, mI) = Prog_Tac.dest_spec spec'
    1.11        val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
    1.12 @@ -27,7 +27,7 @@
    1.13              val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
    1.14  		          handle ERROR "actual args do not match formal args"
    1.15  			          => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
    1.16 -		        val pI' = Refine.refine_ori' init_ctxt pors pI;
    1.17 +		        val pI' = Refine.by_o_model' init_ctxt pors pI;
    1.18  		      in (pI', pors (* refinement over models with diff.precond only *), 
    1.19  		          (hd o #solve_mets o Problem.from_store init_ctxt) pI') end
    1.20  	      else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)