1.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Sun Oct 23 16:08:27 2022 +0200
1.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Sun Oct 23 17:21:04 2022 +0200
1.3 @@ -299,7 +299,7 @@
1.4 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
1.5
1.6 "~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
1.7 - = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
1.8 + = (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
1.9 tac, Celem.Sundef, pt);
1.10 (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
1.11