1.1 --- a/test/Tools/isac/Frontend/use-cases.sml	Thu Oct 20 10:26:29 2016 +0200
     1.2 +++ b/test/Tools/isac/Frontend/use-cases.sml	Thu Oct 27 09:53:54 2016 +0200
     1.3 @@ -619,7 +619,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", @{thm all_left}));
     1.8 + setNextTactic 1 (Rewrite ("all_left", num_str @{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 @@ -1348,7 +1348,7 @@
    1.13   val (Form f, tac, asms) = pt_extract (pt, p);
    1.14   if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
    1.15   error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
    1.16 -DEconstrCalcTree 1;
    1.17 + DEconstrCalcTree 1;
    1.18  
    1.19  "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
    1.20  "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
    1.21 @@ -1370,12 +1370,11 @@
    1.22    val p = get_pos 1 1;
    1.23    val (Form f, _, asms) = pt_extract (pt, p);
    1.24  
    1.25 -  if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
    1.26 +  if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
    1.27    then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
    1.28        ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
    1.29    | _ => error "embed fun get_fillform changed 1"
    1.30  else error "embed fun get_fillform changed 2";
    1.31 -============ inhibit exn WN161019 TODO ========================================================*)
    1.32  
    1.33  (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
    1.34  findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
    1.35 @@ -1437,7 +1436,7 @@
    1.36  "--------- UC errpat add-fraction, fillpat by input --------------";
    1.37  "--------- UC errpat add-fraction, fillpat by input --------------";
    1.38  (*cp from BridgeLog Java <=> SML*)
    1.39 -=CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
    1.40 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
    1.41  Iterator 1;
    1.42  moveActiveRoot 1;
    1.43  moveActiveFormula 1 ([],Pbl);
    1.44 @@ -1454,7 +1453,7 @@
    1.45  "--------- UC errpat, fillpat step to Rewrite --------------------";
    1.46  "--------- UC errpat, fillpat step to Rewrite --------------------";
    1.47  (*TODO*)
    1.48 -=CalcTree
    1.49 +CalcTree
    1.50  [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
    1.51     "differentiateFor x", "derivative f_f'"], 
    1.52    ("Isac", ["derivative_of","function"],