diff -r b79df37bbdc4 -r 9834c21c4ba1 src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Wed Jun 02 11:36:09 2010 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Wed Jun 02 15:35:13 2010 +0200
@@ -236,10 +236,6 @@
 
 end
 
-consts_code
-  "default :: nat" ("{* 0::nat *}")
-  "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-
 definition
   "test n u = pigeonhole n (\<lambda>m. m - 1)"
 definition
@@ -247,6 +243,19 @@
 definition
   "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
 
+ML "timeit (@{code test} 10)" 
+ML "timeit (@{code test'} 10)"
+ML "timeit (@{code test} 20)"
+ML "timeit (@{code test'} 20)"
+ML "timeit (@{code test} 25)"
+ML "timeit (@{code test'} 25)"
+ML "timeit (@{code test} 500)"
+ML "timeit @{code test''}"
+
+consts_code
+  "default :: nat" ("{* 0::nat *}")
+  "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
+
 code_module PH
 contains
   test = test
@@ -254,27 +263,13 @@
   test'' = test''
 
 ML "timeit (PH.test 10)"
-ML "timeit (@{code test} 10)" 
-
 ML "timeit (PH.test' 10)"
-ML "timeit (@{code test'} 10)"
-
 ML "timeit (PH.test 20)"
-ML "timeit (@{code test} 20)"
-
 ML "timeit (PH.test' 20)"
-ML "timeit (@{code test'} 20)"
-
 ML "timeit (PH.test 25)"
-ML "timeit (@{code test} 25)"
-
 ML "timeit (PH.test' 25)"
-ML "timeit (@{code test'} 25)"
-
 ML "timeit (PH.test 500)"
-ML "timeit (@{code test} 500)"
-
 ML "timeit PH.test''"
-ML "timeit @{code test''}"
 
 end
+