1.1 --- a/test/Tools/isac/Interpret/script.sml	Wed Jul 27 09:32:13 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Wed Jul 27 11:57:46 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  "-----------------------------------------------------------------";
     1.5  "-----------------------------------------------------------------";
     1.6  
     1.7 -
     1.8 +val thy= @{theory Isac};
     1.9  "----------- WN0509 why does next_tac doesnt find Substitute -----";
    1.10  "----------- WN0509 why does next_tac doesnt find Substitute -----";
    1.11  "----------- WN0509 why does next_tac doesnt find Substitute -----";
    1.12 @@ -29,10 +29,7 @@
    1.13  "       (M1__M1::bool) = ((Substitute [v_v = 0])) q___q              " ^
    1.14  " in True)";
    1.15  
    1.16 -(*========== inhibit exn 110721 ================================================
    1.17 -(* ERROR: parse thy Can't unify theory to domID * rls*)
    1.18  val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.19 -========= inhibit exn 110721 ================================================*)
    1.20  
    1.21  val str = (*#2#*)
    1.22  "Script BiegelinieScript                                             " ^ 
    1.23 @@ -73,10 +70,8 @@
    1.24  " in True)"
    1.25  ;
    1.26  
    1.27 -(*========== inhibit exn 110721 ================================================
    1.28  val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.29  atomty sc';
    1.30 -========== inhibit exn 110721 ================================================*)
    1.31  
    1.32  val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
    1.33  (*---------------------------------------------------------------------
    1.34 @@ -158,12 +153,8 @@
    1.35  "        M1__M1        = Substitute [e1__e1] M1__M1                  " ^
    1.36  " in True)"
    1.37  ;
    1.38 -(*========== inhibit exn 110721 ================================================
    1.39 -(*---^^^-OK-----------------------------------------------------------------*)
    1.40  val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.41  atomty sc';
    1.42 -(*---vvv-NOT ok-------------------------------------------------------------*)
    1.43 -========== inhibit exn 110721 ================================================*)
    1.44  
    1.45  val str = (*Substitute @@ Substitute does NOT work???*)
    1.46  "Script BiegelinieScript                                             " ^

     2.1 --- a/test/Tools/isac/Interpret/solve.sml	Wed Jul 27 09:32:13 2011 +0200
     2.2 +++ b/test/Tools/isac/Interpret/solve.sml	Wed Jul 27 11:57:46 2011 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4  "-----------------------------------------------------------------";
     2.5  "-----------------------------------------------------------------";
     2.6  
     2.7 -
     2.8 +val thy= @{theory Isac};
     2.9  "--------- interSteps on norm_Rational ---------------------------";
    2.10  "--------- interSteps on norm_Rational ---------------------------";
    2.11  "--------- interSteps on norm_Rational ---------------------------";
    2.12 @@ -254,9 +254,6 @@
    2.13  (---------------WN060614?!?---*)
    2.14  
    2.15   val t = str2term "(3 + x) * (3 + -1 * x)";
    2.16 -(*============ inhibit exn AK110725 ==============================================
    2.17 -(* ERROR: error is only visible in Test_Isac.sml -
    2.18 -   can't unify theory to domID * rls *)
    2.19   val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
    2.20   "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
    2.21   val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
    2.22 @@ -267,7 +264,6 @@
    2.23   "9 + (0 * x + -1 * x ^^^ 2)";
    2.24   val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
    2.25   "9 + - (x ^^^ 2)"; 
    2.26 -============ inhibit exn AK110725 ==============================================*)
    2.27  
    2.28   (*14.3.03*)
    2.29  val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     3.1 --- a/test/Tools/isac/Test_Some.thy	Wed Jul 27 09:32:13 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Jul 27 11:57:46 2011 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  ML{* writeln "**** run the test ***************************************" *}
     3.6  
     3.7 -use"../../../test/Tools/isac/Interpret/appl.sml" 
     3.8 +use"../../../test/Tools/isac/Interpret/script.sml" 
     3.9  
    3.10  ML {*
    3.11