1.1 --- a/test/Tools/isac/OLDTESTS/script.sml	Mon Oct 11 12:55:40 2010 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/script.sml	Mon Oct 11 13:31:22 2010 +0200
     1.3 @@ -186,7 +186,7 @@
     1.4  "--------------------- Notlocatable: Free_Solve ---------------------";
     1.5  val fmz = []; 
     1.6  val (dI',pI',mI') =
     1.7 -  ("Test.thy",["sqroot-test","univariate","equation","test"],
     1.8 +  ("Test",["sqroot-test","univariate","equation","test"],
     1.9     ["Test","sqrt-equ-test"]);
    1.10  (*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
    1.11  val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)
    1.12 @@ -205,7 +205,7 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.14  val nxt = ("Add_Find",Add_Find "solutions v_i_");
    1.15  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.16 -val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
    1.17 +val nxt = ("Specify_Theory",Specify_Theory "Test");
    1.18  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.19  val nxt =
    1.20    ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);
    1.21 @@ -256,12 +256,12 @@
    1.22     \  (Try (Repeat (Rewrite radd_0 False)))))\
    1.23     \ e_e            ");
    1.24  atomty sc;
    1.25 -val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
    1.26 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
    1.27  		     ["Test","sqrt-equ-test"]);
    1.28  val p = e_pos'; val c = []; 
    1.29  val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
    1.30  val (p,_,_,_,_,pt) = me (mI,m) p c  EmptyPtree;
    1.31 -val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
    1.32 +val nxt = ("Specify_Theory",Specify_Theory "Test");
    1.33  val (p,_,_,_,_,pt) = me nxt p c pt;
    1.34  val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
    1.35  val (p,_,_,_,_,pt) = me nxt p c pt;
    1.36 @@ -306,7 +306,7 @@
    1.37   states:=[];
    1.38   CalcTree
    1.39   [(["equality (x+1=2)", "solveFor x","solutions L"], 
    1.40 -   ("Test.thy", 
    1.41 +   ("Test", 
    1.42      ["sqroot-test","univariate","equation","test"],
    1.43      ["Test","squ-equ-test-subpbl1"]))];
    1.44   Iterator 1;
    1.45 @@ -321,7 +321,7 @@
    1.46  
    1.47   val tacs = sel_rules pt ([1],Res);
    1.48   if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.49 -      Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
    1.50 +      Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
    1.51        Check_elementwise "Assumptions"] then ()
    1.52   else error "script.sml: diff.behav. in sel_rules ([1],Res)";
    1.53  
    1.54 @@ -336,7 +336,7 @@
    1.55  
    1.56   val tacs = sel_rules pt ([3],Res);
    1.57   if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
    1.58 -      Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
    1.59 +      Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
    1.60        Check_elementwise "Assumptions"] then ()
    1.61   else error "script.sml: diff.behav. in sel_rules ([3],Res)";
    1.62