1.1 --- a/test/Tools/isac/Test_Some.thy	Sat Oct 05 15:46:30 2019 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Sat Oct 05 15:48:41 2019 +0200
     1.3 @@ -197,20 +197,20 @@
     1.4  "~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (cstate, istate, ctxt, tac)
     1.5    = (*xxxxx_xx*)(**)Safe_Step ((ctree, pos'), Istate.Pstate is, get_ctxt ctree pos', tac')(**);
     1.6  \<close> ML \<open>
     1.7 -(*NEW* )     let
     1.8 +(*NEW*)     let
     1.9  (*NEW*)        val (p'',c',f',pt') =
    1.10  (*NEW*)          Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m
    1.11  (*NEW*)          (* ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
    1.12  (*NEW*)            (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
    1.13  (*NEW*)     in
    1.14 -(*NEW*)		    ("ok", ([(Lucin.tac_2tac tac, tac, p'', (istate, ctxt)))],
    1.15 +(*NEW*)		    ("ok", ([(Lucin.tac_2tac tac, tac, p'', (istate, ctxt))],
    1.16  (*NEW*)         [(*ctree NOT cut*)], (pt', p'')))
    1.17  (*NEW*)
    1.18  (*NEW*)     end
    1.19 -( *NEW*)
    1.20 -(*OLD*)		        ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))],
    1.21 +(*NEW*)
    1.22 +(*OLD* )		        ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))],
    1.23  (*OLD*)             [(*ctree NOT cut*)], cstate))
    1.24 -(*OLD*)
    1.25 +( *OLD*)
    1.26  \<close> ML \<open>
    1.27  
    1.28      ([(tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate); (*return value*)