src/HOL/Code_Evaluation.thy
changeset 55642 63beb38e9258
parent 52435 6646bb548c6b
child 56241 029246729dc0
--- a/src/HOL/Code_Evaluation.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -107,7 +107,7 @@
 
 subsubsection {* Code generator setup *}
 
-lemmas [code del] = term.recs term.cases term.size
+lemmas [code del] = term.rec term.case term.size
 lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
 
 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..