code generator: wfrec combinator is now implemented by ML function wf_rec.

--- a/src/HOL/Main.thy	Fri Apr 19 14:47:10 2002 +0200
+++ b/src/HOL/Main.thy	Fri Apr 19 14:51:33 2002 +0200
@@ -116,6 +116,10 @@
   "Nil"     ("[]")
   "Cons"    ("(_ ::/ _)")
 
+  "wfrec"   ("wf'_rec?")
+
+ML {* fun wf_rec f x = f (wf_rec f) x; *}
+
 lemma [code]: "((n::nat) < 0) = False" by simp
 declare less_Suc_eq [code]