--- a/src/HOL/Fact.thy Mon Feb 23 07:19:53 2009 -0800
+++ b/src/HOL/Fact.thy Mon Feb 23 07:58:13 2009 -0800
@@ -7,7 +7,7 @@
header{*Factorial Function*}
theory Fact
-imports Nat
+imports Main
begin
consts fact :: "nat => nat"
--- a/src/HOL/Plain.thy Mon Feb 23 07:19:53 2009 -0800
+++ b/src/HOL/Plain.thy Mon Feb 23 07:58:13 2009 -0800
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record Extraction Divides Fact
+imports Datatype FunDef Record Extraction Divides
begin
text {*