1.1 --- a/test/Tools/isac/Frontend/use-cases.sml	Sun Oct 16 13:58:46 2016 +0200
     1.2 +++ b/test/Tools/isac/Frontend/use-cases.sml	Tue Oct 18 12:05:03 2016 +0200
     1.3 @@ -621,7 +621,7 @@
     1.4   autoCalculate 1 (Step 1); fetchProposedTactic 1;
     1.5   setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
     1.6   autoCalculate 1 (Step 1); fetchProposedTactic 1;
     1.7 - setNextTactic 1 (Rewrite ("all_left",""));
     1.8 + setNextTactic 1 (Rewrite ("all_left", Thm.prop_of @{thm all_left}));
     1.9   autoCalculate 1 (Step 1); fetchProposedTactic 1;
    1.10   setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
    1.11   autoCalculate 1 (Step 1); fetchProposedTactic 1;
    1.12 @@ -1375,8 +1375,8 @@
    1.13    val (Form f, _, asms) = pt_extract (pt, p);
    1.14  
    1.15    if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
    1.16 -    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], 
    1.17 -      ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
    1.18 +    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
    1.19 +      ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
    1.20    then () else error "embed fun get_fillform changed 1";
    1.21  
    1.22  (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================