diff -r 2b9bfa0b44f1 -r bd4965bb7bdc src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 03 16:33:11 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 03 16:48:36 2010 +0200
@@ -7,9 +7,10 @@
 theory Euclidean_Space
 imports
   Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  Infinite_Set
-  Inner_Product L2_Norm Convex
-uses "positivstellensatz.ML" ("normarith.ML")
+  Infinite_Set Inner_Product L2_Norm Convex
+uses
+  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
+  ("normarith.ML")
 begin
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"