# HG changeset patch
# User Andreas Lochbihler
# Date 1408950525 -7200
# Node ID f8e6197668c96c533173333c4cabde234b448e7a
# Parent  f7be22c6646b5dcb22f182ba92cedf4b64d7b253
correct code equation for term_of on integer

diff -r f7be22c6646b -r f8e6197668c9 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Mon Aug 25 08:45:32 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Aug 25 09:08:45 2014 +0200
@@ -131,10 +131,14 @@
 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))"
+  "term_of (i :: integer) =
+  (if i > 0 then 
+     App (Const (STR ''Num.numeral_class.numeral'') (TYPEREP(num \<Rightarrow> integer)))
+      (term_of (num_of_integer i))
+   else if i = 0 then Const (STR ''Groups.zero_class.zero'') TYPEREP(integer)
+   else
+     App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer))
+       (term_of (- i)))"
 by(rule term_of_anything[THEN meta_eq_to_obj_eq])
 
 code_reserved Eval HOLogic