diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Partial_Function.thy
--- 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)