# HG changeset patch
# User chaieb
# Date 1234193906 0
# Node ID eb7e62c0f53cc969724fac3c37b37faca1e0f715
# Parent  3d935e8b0bf7ce70782f4eea44e307e9ee23ffba
Now imports Fact as suggested by Florian in order to avoid the typerep problem

diff -r 3d935e8b0bf7 -r eb7e62c0f53c src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Mon Feb 09 11:15:13 2009 +0000
+++ b/src/HOL/Plain.thy	Mon Feb 09 15:38:26 2009 +0000
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Record Extraction Divides
+imports Datatype FunDef Record Extraction Divides Fact
 begin
 
 text {*