851 val ctxt = Ctree.get_ctxt pt pos; |
851 val ctxt = Ctree.get_ctxt pt pos; |
852 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
852 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
853 (*if*) p_ = Pos.Pbl (*else*); |
853 (*if*) p_ = Pos.Pbl (*else*); |
854 |
854 |
855 Specify.for_method ctxt oris (o_refs, refs) (pbl, met); |
855 Specify.for_method ctxt oris (o_refs, refs) (pbl, met); |
856 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) |
856 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met)) |
857 = (ctxt, oris, (o_refs, refs), (pbl, met)); |
857 = (ctxt, oris, (o_refs, refs), (pbl, met)); |
858 val cmI = if mI = MethodC.id_empty then mI' else mI; |
858 val cmI = if mI = MethodC.id_empty then mI' else mI; |
859 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*) |
859 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*) |
860 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0; |
860 val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST met); |
861 val NONE = |
861 val NONE = |
862 (*case*) find_first (I_Model.is_error o #5) met (*of*); |
862 (*case*) find_first (I_Model.is_error o #5) met (*of*); |
863 |
863 |
864 (*case*) |
864 (*case*) |
865 Specify.item_to_add (ThyC.get_theory ctxt |
865 Specify.item_to_add (ThyC.get_theory ctxt |