diff -r 119680ebf37c -r 6ebf918128b9 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Nov 12 17:37:43 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Nov 12 17:37:43 2014 +0100
@@ -3494,7 +3494,8 @@
     | term_of_bool false = @{term False};
 
   val mk_int = HOLogic.mk_number @{typ int} o @{code integer_of_int};
-  val dest_int = @{code int_of_integer} o snd o HOLogic.dest_number;
+  fun dest_int (@{term int_of_integer} $ j) = @{code int_of_integer} (snd (HOLogic.dest_number j))
+    | dest_int i = @{code int_of_integer} (snd (HOLogic.dest_number i));
 
   fun term_of_float (@{code Float} (k, l)) =
     @{term Float} $ mk_int k $ mk_int l;
@@ -3706,4 +3707,11 @@
 
 ML_file "approximation.ML"
 
+
+section "Quickcheck Generator"
+
+ML_file "approximation_generator.ML"
+
+setup "Approximation_Generator.setup"
+
 end