src/HOL/Semiring_Normalization.thy

--- a/src/HOL/Semiring_Normalization.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -8,8 +8,6 @@
 imports Numeral_Simprocs Nat_Transfer
 begin
 
-ML_file "Tools/semiring_normalizer.ML"
-
 text {* Prelude *}
 
 class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
@@ -69,7 +67,7 @@
 
 text {* Semiring normalization proper *}
 
-setup Semiring_Normalizer.setup
+ML_file "Tools/semiring_normalizer.ML"
 
 context comm_semiring_1
 begin