# HG changeset patch
# User Andreas Lochbihler
# Date 1408949132 -7200
# Node ID f7be22c6646b5dcb22f182ba92cedf4b64d7b253
# Parent  177eeda93a8cc4c89d59f252e8c10a64b634fbd0# Parent  f23045003476f9e43dc469d060e98a5931341032
merged

diff -r 177eeda93a8c -r f7be22c6646b src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Aug 22 17:35:48 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Aug 25 08:45:32 2014 +0200
@@ -128,6 +128,15 @@
   constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
 | constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
 
+declare [[code drop: "term_of :: integer \<Rightarrow> _"]]
+
+lemma term_of_integer [unfolded typerep_fun_def typerep_num_def typerep_integer_def, code]:
+  "Code_Evaluation.term_of (i :: integer) =
+   Code_Evaluation.App
+    (Code_Evaluation.Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer)))
+    (term_of (num_of_integer i))"
+by(rule term_of_anything[THEN meta_eq_to_obj_eq])
+
 code_reserved Eval HOLogic