src/HOL/Groebner_Basis.thy

--- a/src/HOL/Groebner_Basis.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -6,8 +6,6 @@
 
 theory Groebner_Basis
 imports Semiring_Normalization
-uses
-  ("Tools/groebner.ML")
 begin
 
 subsection {* Groebner Bases *}
@@ -41,7 +39,7 @@
 
 setup Algebra_Simplification.setup
 
-use "Tools/groebner.ML"
+ML_file "Tools/groebner.ML"
 
 method_setup algebra = {*
   let