test/Tools/isac/Minisubpbl/200-start-method.sml
changeset 59571 57ebc51625f2
parent 59562 d50fe358f04a
child 59572 f860c09e856b
     1.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Wed Jul 24 09:48:39 2019 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Wed Jul 24 10:35:19 2019 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  "~~~~~ continue last appy";
     1.5  val Chead.Appl m' = Applicable.applicable_in p pt m;
     1.6  "~~~~~ fun tac_2res, args:"; val (m) = (m');
     1.7 -"~~~~~ fun rep_tac_, args:"; val (Tac.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
     1.8 +"~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
     1.9        val fT = type_of f;
    1.10        val b = if put then @{term True} else @{term False};
    1.11        val lhs = Const ("Script.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)