1.1 --- a/test/Tools/isac/Test_Some.thy	Thu Dec 19 12:40:17 2019 +0100
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Thu Dec 19 16:41:57 2019 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4   = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
     1.5  (* should formulas from calculation really go into ctxt ?                                                     ^^^^^     ^^^^^^^^^*)
     1.6  \<close> ML \<open>
     1.7 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [1], pt);
     1.8 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [1], pt);
     1.9  \<close> ML \<open>
    1.10  	    val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt, p) (*of*);
    1.11  \<close> ML \<open>
    1.12 @@ -222,7 +222,7 @@
    1.13  \<close> ML \<open>
    1.14       Solve.solve m (pt, pos);
    1.15  \<close> ML \<open>
    1.16 -"~~~~~ fun solve , args:"; val (("Check_Postcond", Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
    1.17 +"~~~~~ fun solve , args:"; val (Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
    1.18    = (m, (pt, pos));
    1.19  \<close> ML \<open>
    1.20  \<close> ML \<open>