use was wrong...
--- a/src/HOL/Commutative_Ring.thy Wed Sep 14 19:03:16 2005 +0200
+++ b/src/HOL/Commutative_Ring.thy Wed Sep 14 21:35:46 2005 +0200
@@ -7,7 +7,7 @@
theory Commutative_Ring
imports List
-uses ("comm_ring.ML")
+uses ("Tools/comm_ring.ML")
begin
(* Syntax of multivariate polynomials (pol) and polynomial expressions*)
@@ -304,7 +304,7 @@
generate_code ("ring.ML") test = "norm"*)
- use "comm_ring.ML"
+ use "Tools/comm_ring.ML"
setup "CommRing.setup"
-end
\ No newline at end of file
+end