
diff -r 787b39d499cf -r 126701134811 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Mar 30 17:14:44 2009 +0200
+++ b/src/HOL/Int.thy	Mon Mar 30 10:47:41 2009 -0700
@@ -12,7 +12,7 @@
 uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
-  ("~~/src/Provers/Arith/assoc_fold.ML")
+  "~~/src/Provers/Arith/assoc_fold.ML"
   "~~/src/Provers/Arith/cancel_numerals.ML"
   "~~/src/Provers/Arith/combine_numerals.ML"
   ("Tools/int_arith.ML")
@@ -1525,7 +1525,6 @@
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
 
-use "~~/src/Provers/Arith/assoc_fold.ML"
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
 




