--- a/src/HOL/Meson.thy Mon Oct 04 22:01:34 2010 +0200
+++ b/src/HOL/Meson.thy Mon Oct 04 22:45:09 2010 +0200
@@ -8,7 +8,7 @@
header {* MESON Proof Procedure (Model Elimination) *}
theory Meson
-imports Nat
+imports Datatype
uses ("Tools/Meson/meson.ML")
("Tools/Meson/meson_clausify.ML")
begin