--- a/src/HOL/Partial_Function.thy Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Partial_Function.thy Mon Nov 09 15:48:17 2015 +0100
@@ -281,12 +281,12 @@
lemma antisymP_flat_ord: "antisymP (flat_ord a)"
by(rule antisymI)(auto dest: flat_ord_antisym)
-interpretation tailrec!:
+interpretation tailrec:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"
rewrites "flat_lub undefined {} \<equiv> undefined"
by (rule flat_interpretation)(simp add: flat_lub_def)
-interpretation option!:
+interpretation option:
partial_function_definitions "flat_ord None" "flat_lub None"
rewrites "flat_lub None {} \<equiv> None"
by (rule flat_interpretation)(simp add: flat_lub_def)