# HG changeset patch
# User Andreas Lochbihler
# Date 1396610546 -7200
# Node ID 6d9a24f8746073f7e15c7a1420e6345bc26b4d55
# Parent  f0bd809b5d35f827fb8f3c22c8c00970b407b96d# Parent  3b2db6132bfd9882783efad41d846e659f5e936f
merged

diff -r f0bd809b5d35 -r 6d9a24f87460 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Apr 04 12:37:57 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Apr 04 13:22:26 2014 +0200
@@ -275,6 +275,26 @@
      else Code_Evaluation.term_of ((i + 1) div 2))"
   by (rule partial_term_of_anything)+
 
+code_printing constant "Code_Evaluation.term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Haskell_Quickcheck) 
+  "(let { t = Typerep.Typerep \"Code'_Numeral.integer\" [];
+     mkFunT s t = Typerep.Typerep \"fun\" [s, t];
+     numT = Typerep.Typerep \"Num.num\" [];
+     mkBit 0 = Generated'_Code.Const \"Num.num.Bit0\" (mkFunT numT numT);
+     mkBit 1 = Generated'_Code.Const \"Num.num.Bit1\" (mkFunT numT numT);
+     mkNumeral 1 = Generated'_Code.Const \"Num.num.One\" numT;
+     mkNumeral i = let { q = i `Prelude.div` 2; r = i `Prelude.mod` 2 }
+       in Generated'_Code.App (mkBit r) (mkNumeral q);
+     mkNumber 0 = Generated'_Code.Const \"Groups.zero'_class.zero\" t;
+     mkNumber 1 = Generated'_Code.Const \"Groups.one'_class.one\" t;
+     mkNumber i = if i > 0 then
+         Generated'_Code.App
+           (Generated'_Code.Const \"Num.numeral'_class.numeral\"
+              (mkFunT numT t))
+           (mkNumeral i)
+       else
+         Generated'_Code.App
+           (Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t))
+           (mkNumber (- i)); } in mkNumber)"
 
 subsection {* The @{text find_unused_assms} command *}