1.1 --- a/test/Tools/isac/Interpret/inform.sml	Tue Jul 26 15:52:07 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Wed Jul 27 08:43:58 2011 +0200
     1.3 @@ -63,13 +63,13 @@
     1.4   val str = pr_ptree pr_short pt;
     1.5  
     1.6   writeln str;
     1.7 -(*============ inhibit exn AK110725 ==============================================
     1.8 +(*============ inhibit exn AK110726 ==============================================
     1.9  (* 2nd string should be the same as 1st one *)
    1.10  ".    ----- 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";
    1.11  ".    ----- 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";
    1.12   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 ()
    1.13 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
    1.14 -============ inhibit exn AK110725 ==============================================*)
    1.15 +   else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
    1.16 +============ inhibit exn AK110726 ==============================================*)
    1.17  
    1.18   moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
    1.19   moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
    1.20 @@ -87,12 +87,14 @@
    1.21   else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
    1.22  
    1.23   fetchProposedTactic 1; (*takes Iterator 1 _1_*)
    1.24 +
    1.25  (*============ inhibit exn AK110725 ==============================================
    1.26  (* ERROR: exception Bind raised *)
    1.27   val (_,(tac,_,_)::_) = get_calc 1;
    1.28   if tac = Rewrite_Set "Test_simplify" then ()
    1.29   else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
    1.30  ============ inhibit exn AK110725 ==============================================*)
    1.31 +
    1.32   autoCalculate 1 CompleteCalc;
    1.33   val ((pt,_),_) = get_calc 1;
    1.34   if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
    1.35 @@ -529,8 +531,10 @@
    1.36  spec;
    1.37  writeln (itms2str_ ctxt probl);
    1.38  writeln (itms2str_ ctxt meth);
    1.39 +
    1.40  (*============ inhibit exn AK110725 ==============================================
    1.41 -(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
    1.42 +(* ERROR: Argument: istate : istate * Proof.context Reason: 
    1.43 +        Can't unify istate to istate * Proof.context *)
    1.44  writeln (istate2str istate);
    1.45  ============ inhibit exn AK110725 ==============================================*)
    1.46