diff -r 3ef5679743fb -r a12b724f1d37 test/Tools/isac/Interpret/inform.sml
--- a/test/Tools/isac/Interpret/inform.sml	Tue Jul 26 15:52:07 2011 +0200
+++ b/test/Tools/isac/Interpret/inform.sml	Wed Jul 27 08:43:58 2011 +0200
@@ -63,13 +63,13 @@
  val str = pr_ptree pr_short pt;
 
  writeln str;
-(*============ inhibit exn AK110725 ==============================================
+(*============ inhibit exn AK110726 ==============================================
 (* 2nd string should be the same as 1st one *)
 ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   1 + x + -1 * 2 = 0\n2.3.   1 + (x + -1 * 2) = 0\n2.4.   1 + (x + -2) = 0\n2.5.   1 + (x + -2 * 1) = 0\n2.6.   1 + x + -2 * 1 = 0\n";
 ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n";
  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then ()
- else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
-============ inhibit exn AK110725 ==============================================*)
+   else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
+============ inhibit exn AK110726 ==============================================*)
 
  moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
  moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
@@ -87,12 +87,14 @@
  else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
 
  fetchProposedTactic 1; (*takes Iterator 1 _1_*)
+
 (*============ inhibit exn AK110725 ==============================================
 (* ERROR: exception Bind raised *)
  val (_,(tac,_,_)::_) = get_calc 1;
  if tac = Rewrite_Set "Test_simplify" then ()
  else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
 ============ inhibit exn AK110725 ==============================================*)
+
  autoCalculate 1 CompleteCalc;
  val ((pt,_),_) = get_calc 1;
  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
@@ -529,8 +531,10 @@
 spec;
 writeln (itms2str_ ctxt probl);
 writeln (itms2str_ ctxt meth);
+
 (*============ inhibit exn AK110725 ==============================================
-(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
+(* ERROR: Argument: istate : istate * Proof.context Reason: 
+        Can't unify istate to istate * Proof.context *)
 writeln (istate2str istate);
 ============ inhibit exn AK110725 ==============================================*)