equal
deleted
inserted
replaced
12 fun common_sub_thy (thy1, thy2) = |
12 fun common_sub_thy (thy1, thy2) = |
13 if Context.subthy (thy1, thy2) then thy2 |
13 if Context.subthy (thy1, thy2) then thy2 |
14 else if Context.subthy (thy2, thy1) then thy1 |
14 else if Context.subthy (thy2, thy1) then thy1 |
15 else Know_Store.get_ref_last_thy () |
15 else Know_Store.get_ref_last_thy () |
16 |
16 |
17 fun tac_from_prog (pt, p) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') = |
17 fun tac_from_prog (pt, _) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') = |
18 let |
18 let |
19 val (dI, pI, mI) = Prog_Tac.dest_spec spec' |
19 val (dI, pI, mI) = Prog_Tac.dest_spec spec' |
20 val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt); |
20 val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt); |
21 val init_ctxt = Proof_Context.init_global thy |
21 val init_ctxt = Proof_Context.init_global thy |
22 val ags = TermC.isalist2list ags'; |
22 val ags = TermC.isalist2list ags'; |
25 then |
25 then |
26 let |
26 let |
27 val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T |
27 val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T |
28 handle ERROR "actual args do not match formal args" |
28 handle ERROR "actual args do not match formal args" |
29 => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]); |
29 => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]); |
30 val pI' = Refine.refine_ori' init_ctxt pors pI; |
30 val pI' = Refine.by_o_model' init_ctxt pors pI; |
31 in (pI', pors (* refinement over models with diff.precond only *), |
31 in (pI', pors (* refinement over models with diff.precond only *), |
32 (hd o #solve_mets o Problem.from_store init_ctxt) pI') end |
32 (hd o #solve_mets o Problem.from_store init_ctxt) pI') end |
33 else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags) |
33 else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags) |
34 handle ERROR "actual args do not match formal args" |
34 handle ERROR "actual args do not match formal args" |
35 => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI); |
35 => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI); |