src/HOL/Code_Evaluation.thy
changeset 46664 1f6c140f9c72
parent 46638 fc315796794e
child 47108 2a1953f0d20d
--- a/src/HOL/Code_Evaluation.thy	Fri Feb 24 22:46:16 2012 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 24 22:46:44 2012 +0100
@@ -5,7 +5,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Evaluation
-imports Plain Typerep Code_Numeral
+imports Plain Typerep Code_Numeral Predicate
 uses ("Tools/code_evaluation.ML")
 begin