diff -r 352c73a689da -r c3d6e570ccef src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Partial_Function.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -283,12 +283,12 @@
 
 interpretation tailrec!:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
-  where "flat_lub undefined {} \<equiv> undefined"
+  rewrites "flat_lub undefined {} \<equiv> undefined"
 by (rule flat_interpretation)(simp add: flat_lub_def)
 
 interpretation option!:
   partial_function_definitions "flat_ord None" "flat_lub None"
-  where "flat_lub None {} \<equiv> None"
+  rewrites "flat_lub None {} \<equiv> None"
 by (rule flat_interpretation)(simp add: flat_lub_def)