--- a/src/HOL/Partial_Function.thy Mon May 30 17:55:34 2011 +0200
+++ b/src/HOL/Partial_Function.thy Mon May 23 21:34:37 2011 +0200
@@ -224,10 +224,10 @@
by (rule flat_interpretation)
declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
- @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} *}
+ @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
declaration {* Partial_Function.init "option" @{term option.fixp_fun}
- @{term option.mono_body} @{thm option.fixp_rule_uc} *}
+ @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *}
abbreviation "option_ord \<equiv> flat_ord None"