diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/DiffApp-scrpbl.sml
--- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Sep 08 16:45:27 2010 +0200
+++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Wed Sep 08 16:47:22 2010 +0200
@@ -315,7 +315,7 @@
  "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
  "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
 val (dI',pI',mI')=
-  ("DiffAppl.thy",["Script.thy","maximum_of","function"],e_metID);
+  ("DiffAppl",["Script","maximum_of","function"],e_metID);
 val c = []:cid;
 
 (*
@@ -416,7 +416,7 @@
 	   "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
 	   "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
 val (dI',pI',mI')=
-  ("DiffAppl.thy",["DiffAppl.thy","test_maximum"],e_metID);
+  ("DiffAppl",["DiffAppl","test_maximum"],e_metID);
 val p = e_pos'; val c = []; 
 
 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));