diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Lifting_Set.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -150,12 +150,12 @@
   unfolding rel_fun_def rel_set_def by fast
 
 lemma SUP_parametric [transfer_rule]:
-  "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
+  "(rel_set R ===> (R ===> op =) ===> op =) SUPREMUM (SUPREMUM :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
 proof(rule rel_funI)+
   fix A B f and g :: "'b \<Rightarrow> 'c"
   assume AB: "rel_set R A B"
     and fg: "(R ===> op =) f g"
-  show "SUPR A f = SUPR B g"
+  show "SUPREMUM A f = SUPREMUM B g"
     by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
 qed