# HG changeset patch
# User huffman
# Date 1313617379 25200
# Node ID b922e91dd1d9c632550ad46437fc754cbe7b74e5
# Parent  c478cd500dc4be56f1ec7e4343189c12555dfc7a
Wfrec.thy: respect set/pred distinction

diff -r c478cd500dc4 -r b922e91dd1d9 src/HOL/Library/Wfrec.thy
--- a/src/HOL/Library/Wfrec.thy	Wed Aug 17 14:32:48 2011 -0700
+++ b/src/HOL/Library/Wfrec.thy	Wed Aug 17 14:42:59 2011 -0700
@@ -76,12 +76,12 @@
 
 subsection {* Nitpick setup *}
 
-axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
-definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
 [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
 
-definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
 "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
                 else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"