# HG changeset patch
# User chaieb
# Date 1126726546 -7200
# Node ID 8d143599daa97b27092b3dc0963dc5a28b943d05
# Parent  85109eec887b4f20028e15485f856b916887d0b3
use was wrong...

diff -r 85109eec887b -r 8d143599daa9 src/HOL/Commutative_Ring.thy
--- 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