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)