1.1 --- a/test/Tools/isac/Frontend/use-cases.sml	Thu Jul 24 15:44:50 2014 +0200
     1.2 +++ b/test/Tools/isac/Frontend/use-cases.sml	Thu Jul 24 17:22:21 2014 +0200
     1.3 @@ -1364,7 +1364,8 @@
     1.4    val (Form f, _, asms) = pt_extract (pt, p);
     1.5  
     1.6    if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
     1.7 -    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
     1.8 +    get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], 
     1.9 +      ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
    1.10    then () else error "embed fun get_fillform changed 1";
    1.11  
    1.12  (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================