diff -r 97b5b13937e1 -r 3573fd729e99 test/Tools/isac/Interpret/inform.sml
--- a/test/Tools/isac/Interpret/inform.sml	Sun Jul 24 19:38:53 2011 +0200
+++ b/test/Tools/isac/Interpret/inform.sml	Mon Jul 25 11:52:07 2011 +0200
@@ -1,6 +1,5 @@
-(* tests on inform.sml
-   author: Walther Neuper
-   060225,
+(* Title: tests on inform.sml
+   Author: Walther Neuper 060225,
    (c) due to copyright terms 
 
 use"../smltest/ME/inform.sml";
@@ -44,6 +43,7 @@
 "--------- appendFormula: on Res + equ_nrls ----------------------";
 "--------- appendFormula: on Res + equ_nrls ----------------------";
 "--------- appendFormula: on Res + equ_nrls ----------------------";
+
  val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
  (writeln o term2str) sc;
  val Script sc = (#scr o get_met) ["Test","solve_linear"];
@@ -61,9 +61,15 @@
  appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
+
  writeln str;
+(*============ inhibit exn AK110725 ==============================================
+(* 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 ==============================================*)
 
  moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
  moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
@@ -81,9 +87,12 @@
  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 ()
@@ -100,18 +109,19 @@
 
    *)
 "----------------------------------------------------------";
- val fod = make_deriv (theory "Isac") Atools_erls 
+
+ val fod = make_deriv (@{theory "Isac"}) Atools_erls 
 		       ((#rules o rep_rls) Test_simplify)
-		       (sqrt_right false (theory "Pure")) NONE 
+		       (sqrt_right false (@{theory "Pure"})) NONE 
 		       (str2term "x + 1 + -1 * 2 = 0");
  (writeln o trtas2str) fod;
 
- val ifod = make_deriv (theory "Isac") Atools_erls 
+ val ifod = make_deriv (@{theory "Isac"}) Atools_erls 
 		       ((#rules o rep_rls) Test_simplify)
-		       (sqrt_right false (theory "Pure")) NONE 
+		       (sqrt_right false (@{theory "Pure"})) NONE 
 		       (str2term "-2 * 1 + (1 + x) = 0");
  (writeln o trtas2str) ifod;
- fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;
+ fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
  val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
  val der = fod' @ (map rev_deriv' rifod');
  (writeln o trtas2str) der;
@@ -128,7 +138,6 @@
  Iterator 1; moveActiveRoot 1;
  autoCalculate 1 CompleteCalcHead;
  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
-
  appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
 
  moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
@@ -203,7 +212,7 @@
  if str = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n3.2.   x = 0 + -1 * -1\n3.2.1.   x = 0 + -1 * -1\n3.2.2.   x = 0 + 1\n" andalso p = ([3,2], Res)
  then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
  else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
- 
+
  fetchProposedTactic 1;
  val (_,(tac,_,_)::_) = get_calc 1;
  if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
@@ -256,11 +265,18 @@
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
  writeln str;
- 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()
+
+(*============ inhibit exn AK110725 ==============================================
+(* 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.replaceFormula: on Res += 1";
+============ inhibit exn AK110725 ==============================================*)
+
  autoCalculate 1 CompleteCalc;
- val ((pt,pos as(p,_)),_) = get_calc 1;
- if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
+ val ((pt,pos as (p,_)),_) = get_calc 1;
+ if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
  else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
  
 
@@ -280,11 +296,11 @@
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
  writeln str;
- if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
+ if str= ".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
  else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
  autoCalculate 1 CompleteCalc;
- val ((pt,pos as(p,_)),_) = get_calc 1;
- if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
+ val ((pt,pos as (p,_)),_) = get_calc 1;
+ if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
  else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
 
 
@@ -303,11 +319,11 @@
  val ((pt,_),_) = get_calc 1;
  val str = pr_ptree pr_short pt;
  writeln str;
- if str=".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
+ if str= ".    ----- pblobj -----\n1.   x + 1 = 2\n1.1.   x + 1 = 2\n1.2.   1 + x = 2\n1.3.   1 + x = -2 + 4\n1.4.   x + 1 = -2 + 4\n" then ()
  else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
  autoCalculate 1 CompleteCalc;
- val ((pt,pos as(p,_)),_) = get_calc 1;
- if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
+ val ((pt,pos as (p,_)),_) = get_calc 1;
+ if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
  else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
 
 
@@ -332,7 +348,6 @@
  else error "inform.sml: diff.behav. cut calculation 2";
 
 
-
 (* 040307 copied from informtest.sml; ... old version 
  "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
  "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
@@ -514,7 +529,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 *)
 writeln (istate2str istate);
+============ inhibit exn AK110725 ==============================================*)
 
 print_depth 3;
 
@@ -529,7 +547,10 @@
 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
 val NONE = env;
 val (SOME istate, NONE) = loc;
+(*============ inhibit exn AK110725 ==============================================
+(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
 print_depth 5; writeln (istate2str istate);  print_depth 3;
+============ inhibit exn AK110725 ==============================================*)
 (*ScrState ([],
  [], NONE,
  ??.empty, Sundef, false)*)
@@ -541,12 +562,12 @@
 (*[
 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
-(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
+(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
 writeln (itms2str_ ctxt meth);
 (*[
 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
-(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
+(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
 writeln"-----------------------------------------------------------";
 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
@@ -564,17 +585,19 @@
 (*the following input is copied from BridgeLog Java <==> SML,
   omitting unnecessary inputs*)
 (*1>*)states:=[];
-(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
+(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
 (*3>*)Iterator 1; moveActiveRoot 1;
 
 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
-
 (***difference II***)
 val ((pt,_),_) = get_calc 1;
 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
 val NONE = env;
 val (SOME istate, NONE) = loc;
+(*============ inhibit exn AK110725 ==============================================
+(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
 print_depth 5; writeln (istate2str istate);  print_depth 3;
+============ inhibit exn AK110725 ==============================================*)
 (*ScrState ([],
  [], NONE,
  ??.empty, Sundef, false)*)
@@ -586,15 +609,14 @@
 (*[
 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
-(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
+(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
 writeln (itms2str_ ctxt meth);
 (*[
 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
-(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
+(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
 writeln"-----------------------------------------------------------";
 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
-
 autoCalculate 1 (Step 1);
 val ((pt,p),_) = get_calc 1;
 val Form res = (#1 o pt_extract) (pt, p);