test/Tools/isac/BaseDefinitions/contextC.sml
changeset 60577 ca9f84786137
parent 60571 19a172de0bb5
child 60586 007ef64dbb08
     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