1.1 --- a/src/HOL/Library/Wfrec.thy	Wed Aug 17 14:32:48 2011 -0700
     1.2 +++ b/src/HOL/Library/Wfrec.thy	Wed Aug 17 14:42:59 2011 -0700
     1.3 @@ -76,12 +76,12 @@
     1.4  
     1.5  subsection {* Nitpick setup *}
     1.6  
     1.7 -axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.8 +axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.9  
    1.10 -definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.11 +definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.12  [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
    1.13  
    1.14 -definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.15 +definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.16  "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    1.17                  else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    1.18