--- a/src/HOL/Nat.thy Tue May 31 18:31:33 2016 +0200
+++ b/src/HOL/Nat.thy Tue May 31 19:51:01 2016 +0200
@@ -11,8 +11,6 @@
imports Inductive Typedef Fun Rings
begin
-ML_file "~~/src/Tools/rat.ML"
-
named_theorems arith "arith facts -- only ground formulas"
ML_file "Tools/arith_data.ML"