equal
deleted
inserted
replaced
155 in |
155 in |
156 case I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct of |
156 case I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct of |
157 I_Model.Add i_single => (*..union old input *) |
157 I_Model.Add i_single => (*..union old input *) |
158 let |
158 let |
159 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model |
159 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model |
160 val tac' = I_Model.make_tactic m_field (ct, I_Model.TEST_to_OLD i_model') |
160 val tac' = I_Model.make_tactic m_field (ct, i_model') |
161 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos) |
161 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos) |
162 in |
162 in |
163 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))], |
163 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))], |
164 [], (pt', pos))) |
164 [], (pt', pos))) |
165 end |
165 end |