diff -r 293a30867f15 -r ad0485155c0e test/Tools/isac/OLDTESTS/root-equ.sml
--- a/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Oct 11 12:55:40 2010 +0200
+++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Mon Oct 11 13:31:22 2010 +0200
@@ -40,7 +40,7 @@
 " _________________ equation with x =(-12)/5, but L ={} ------- ";
 (*                  -------------------------------------         *)
 " _________________ rewrite _________________ ";
-val thy' = "Test.thy";
+val thy' = "Test";
 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
 val thm = ("square_equation_left","");
 val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
@@ -213,7 +213,7 @@
 atomty ((#prop o rep_thm) (!tthm));
 atomty (term_of (!tct));
 *)
-val thy' = "Test.thy";
+val thy' = "Test";
 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
 (*1*)val thm = ("square_equation_left","");
 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
@@ -257,7 +257,7 @@
 " _________________ rewrite + cappend _________________ ";
 " _________________ rewrite + cappend _________________ ";
 " _________________ rewrite + cappend _________________ ";
-val thy' = "Test.thy";
+val thy' = "Test";
 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
 val oris = prep_ori ctl thy 
@@ -400,8 +400,8 @@
 	   "solutions L"(*,
       "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
 val (dI',pI',mI') =
-  ("Test.thy",["sqroot-test","univariate","equation","test"],
-   ("Test.thy","sqrt-equ-test"));
+  ("Test",["sqroot-test","univariate","equation","test"],
+   ("Test","sqrt-equ-test"));
 val p = e_pos'; val c = []; 
 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
 
@@ -414,15 +414,15 @@
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl.thy");
+(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
 > get_obj g_spec pt (fst p);
 val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 (*val nxt = ("Specify_Problem", Specify_Problem *)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*)
+(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
-(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*)
+(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)
 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
 val nxt = ("Free_Solve",Free_Solve);
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
@@ -488,9 +488,9 @@
 val ((p,p_),_,f,nxt,_,pt)=
 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
 (* 5.4.00.: ---
-get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt;
+get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;
 val (p,_,f,nxt,_,pt)=
-me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt;
+me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
 --- *) 
 writeln (pr_ptree pr_short pt);
 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
@@ -504,7 +504,7 @@
 	   "solveFor x","errorBound (eps=0)",
 	   "solutions L"];
 val (dI',pI',mI') =
-  ("Test.thy",["sqroot-test","univariate","equation","test"],
+  ("Test",["sqroot-test","univariate","equation","test"],
    ["Test","sqrt-equ-test"]);
 "--- s1 ---";
 (*val p = e_pos'; val c = []; 
@@ -529,7 +529,7 @@
 val nxt = ("Add_Find",Add_Find "solutions L");
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 "--- s6 ---";
-val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
+val nxt = ("Specify_Theory",Specify_Theory "Test");
 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 "--- s7 ---";
 val nxt = ("Specify_Problem",