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 *}