adding code_unfold to make measure executable

--- a/src/HOL/Wellfounded.thy	Sun Jan 29 15:16:27 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Jan 30 13:55:19 2012 +0100
@@ -635,7 +635,7 @@
 definition measure :: "('a => nat) => ('a * 'a)set"
 where "measure = inv_image less_than"
 
-lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
+lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)"
   by (simp add:measure_def)
 
 lemma wf_measure [iff]: "wf (measure f)"