--- a/src/HOL/ex/Fundefs.thy Mon Sep 19 23:34:22 2011 +0200
+++ b/src/HOL/ex/Fundefs.thy Tue Sep 20 01:32:04 2011 +0200
@@ -387,4 +387,9 @@
| "f4 _ _ = False"
+(* polymorphic partial_function *)
+partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
+where
+ "f5 x = f5 x"
+
end