--- a/src/HOL/Partial_Function.thy Wed Dec 21 21:26:26 2016 +0100
+++ b/src/HOL/Partial_Function.thy Thu Dec 22 08:43:30 2016 +0100
@@ -283,8 +283,8 @@
lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
by(auto simp add: flat_ord_def)
-lemma antisymP_flat_ord: "antisymP (flat_ord a)"
-by(rule antisymI)(auto dest: flat_ord_antisym)
+lemma antisymp_flat_ord: "antisymp (flat_ord a)"
+by(rule antisympI)(auto dest: flat_ord_antisym)
interpretation tailrec:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"