changeset 21545 | 54cc492d80a9 |
parent 21404 | eb85850d3eb7 |
child 22507 | 3572bc633d9a |
--- a/src/HOL/Extraction/Pigeonhole.thy Mon Nov 27 12:12:18 2006 +0100 +++ b/src/HOL/Extraction/Pigeonhole.thy Mon Nov 27 13:42:30 2006 +0100 @@ -316,7 +316,7 @@ definition "test' n = pigeonhole_slow n (\<lambda>m. m - 1)" -code_gen test test' "op !" (SML *) +code_gen test test' "op !" (SML #) ML "timeit (fn () => ROOT.Pigeonhole.test 10)" ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"