1.1 --- a/test/Tools/isac/Interpret/inform.sml	Sat Jul 26 13:39:00 2014 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Sat Jul 26 14:10:05 2014 +0200
     1.3 @@ -1252,8 +1252,8 @@
     1.4    val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
     1.5    val p' = lev_on p;
     1.6    val tac = get_obj g_tac pt p';
     1.7 -  if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) then ()
     1.8 -  else error "inputFillFormula changed 10";
     1.9 +if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
    1.10 +then () else error "inputFillFormula changed 10";
    1.11    val Appl rew = applicable_in pos pt tac;
    1.12    val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
    1.13  
    1.14 @@ -1269,6 +1269,7 @@
    1.15  val (Form f, _, asms) = pt_extract (pt, p);
    1.16  if p = ([2], Res) andalso
    1.17    term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
    1.18 -  get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
    1.19 +  get_obj g_tac pt (fst p) =
    1.20 +    Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
    1.21  then () else error "inputFillFormula changed 11";
    1.22