--- 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)