diff -r 09a757ca128f -r dfd31c1db060 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Tue Mar 10 18:52:26 2009 +0100
+++ b/src/HOL/Code_Eval.thy	Wed Mar 11 08:45:46 2009 +0100
@@ -134,6 +134,10 @@
 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
 lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]:
+  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
+lemma [code, code del]:
+  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
     (let (n, m) = nibble_pair_of_char c