src/HOL/Code_Evaluation.thy
changeset 46635 cde737f9c911
parent 42979 5b9e16259341
child 46638 fc315796794e
--- a/src/HOL/Code_Evaluation.thy	Thu Feb 23 21:16:54 2012 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Feb 23 21:25:59 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