# HG changeset patch
# User blanchet
# Date 1256815771 -3600
# Node ID 3b8fc89a52b78e7254ff6a57eb33f972be615ee5
# Parent  1c62ac4ef6d17e308314d0a0d9751e7b72b83d71
readded Predicate_Compile to Main

diff -r 1c62ac4ef6d1 -r 3b8fc89a52b7 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Oct 29 12:09:32 2009 +0100
+++ b/src/HOL/Main.thy	Thu Oct 29 12:29:31 2009 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Nitpick
+imports Plain Nitpick Predicate_Compile
 begin
 
 text {*