--- a/src/HOL/Plain.thy Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Plain.thy Sun Mar 25 20:15:39 2012 +0200
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Extraction Metis
+imports Datatype FunDef Extraction Metis Num
begin
text {*