1.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -710,7 +710,7 @@
     1.4   autoCalculate 1 (Steps 1); fetchProposedTactic 1;
     1.5   setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
     1.6   autoCalculate 1 (Steps 1); fetchProposedTactic 1;
     1.7 - setNextTactic 1 (Rewrite ("all_left", ThmC.numerals_to_Free @{thm all_left}));
     1.8 + setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
     1.9   autoCalculate 1 (Steps 1); fetchProposedTactic 1;
    1.10   setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
    1.11   autoCalculate 1 (Steps 1); fetchProposedTactic 1;