diff -r d28a071bb6db -r aaca5c033fa4 test/Tools/isac/Interpret/inform.sml
--- a/test/Tools/isac/Interpret/inform.sml	Thu May 17 16:44:13 2012 +0200
+++ b/test/Tools/isac/Interpret/inform.sml	Thu May 17 19:09:48 2012 +0200
@@ -33,6 +33,8 @@
 "--------- init_form, start with <NEW> (CAS input) ---------------";
 "--------- build fun check_err_patt ------------------------------";
 "--------- build fun check_err_patt ?bdv -------------------------";
+"--------- build fun check_error_patterns ------------------------";
+"--------- embed fun check_error_patterns ------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
@@ -869,4 +871,88 @@
 if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
 then () else error "error patt example1 changed";
 
+"--------- build fun check_error_patterns ------------------------";
+"--------- build fun check_error_patterns ------------------------";
+"--------- build fun check_error_patterns ------------------------";
+val (res, inf) =
+  (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
+   str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
+val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
 
+val env = [(str2term "v_v", str2term "x")];
+val errpats =
+  [e_errpat, (*generalised for testing*)
+   ("chain-rule-diff-both",
+     [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
+      parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
+      parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
+      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
+      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
+     [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 
+      @{thm diff_ln_chain}, @{thm  diff_exp_chain}])]: errpat list;
+
+case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => () 
+| NONE => error "check_error_patterns broken";
+
+
+"--------- embed fun check_error_patterns ------------------------";
+"--------- embed fun check_error_patterns ------------------------";
+"--------- embed fun check_error_patterns ------------------------";
+states:=[];
+CalcTree
+[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 
+  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
+Iterator 1;
+moveActiveRoot 1;
+autoCalculate 1 CompleteCalcHead;
+autoCalculate 1 (Step 1);
+autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
+(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
+
+"~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
+val cs = get_calc cI
+val pos as (_,p_) = get_pos cI 1; (*pos = ([1], Res)*)
+val cs' = 
+    case step pos cs of
+	    ("ok", cs') => cs';
+
+val (_, _, (pt, ([2], Res))) = cs';
+(*show_pt pt;
+  [(([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
+   (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
+   (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)"
+   (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *)
+
+"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
+  (cs', (encode ifo));
+val 	SOME f_in = parse (assoc_thy "Isac") istr
+val f_in = term_of f_in
+val pos_pred = lev_back' pos
+			(* f_pred ---"step pos cs"---> f_succ in appendFormula
+   TODO.WN120517: one starting point for redesign of pos' *)
+val (f_pred, f_succ) = (get_pred_formula (pt, pos_pred), get_pred_formula (pt, pos));
+	
+term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))";
+term2str f_succ = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";
+
+			f_succ = f_in; (* = false*)
+cas_input f_in; (* = NONE*)
+val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
+val ("no derivation found", calcstate') = msg_calcstate';
+			                 val pp = par_pblobj pt p
+			                 val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
+			                 val ScrState (env, _, _, _, _, _) = get_istate pt pos;
+                 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
+			                   SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
+			                 | NONE => msg_calcstate';
+
+"~~~~~ from inform return val:"; val () = ();
+case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
+			  SOME errpatID => ()
+			| NONE => error "check_error_patterns broken";
+
+"--- final check:";
+case inform cs' (encode ifo) of
+  ("error pattern #chain-rule-diff-both#", calcstate') => ()
+| _ => error "inform with (positive) check_error_patterns broken"
+