--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Aug 22 22:55:41 2012 +0200
@@ -7,7 +7,6 @@
theory Commutative_Ring
imports Main Parity
-uses ("commutative_ring_tac.ML")
begin
text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
@@ -313,7 +312,7 @@
qed
-use "commutative_ring_tac.ML"
+ML_file "commutative_ring_tac.ML"
method_setup comm_ring = {*
Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)