diff -r 455a9f89c47d -r 7aa35601ff65 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu May 24 14:20:23 2012 +0200
@@ -21,9 +21,9 @@
 
   val get_invariant_commute_rules: Proof.context -> thm list
   
-  val get_reflp_preserve_rules: Proof.context -> thm list
-  val add_reflp_preserve_rule_attribute: attribute
-  val add_reflp_preserve_rule_attrib: Attrib.src
+  val get_reflexivity_rules: Proof.context -> thm list
+  val add_reflexivity_rule_attribute: attribute
+  val add_reflexivity_rule_attrib: Attrib.src
 
   val setup: theory -> theory
 end;
@@ -183,13 +183,13 @@
 
 structure Reflp_Preserve = Named_Thms
 (
-  val name = @{binding reflp_preserve}
+  val name = @{binding reflexivity_rule}
   val description = "theorems that a relator preserves a reflexivity property"
 )
 
-val get_reflp_preserve_rules = Reflp_Preserve.get
-val add_reflp_preserve_rule_attribute = Reflp_Preserve.add
-val add_reflp_preserve_rule_attrib = Attrib.internal (K add_reflp_preserve_rule_attribute)
+val get_reflexivity_rules = Reflp_Preserve.get
+val add_reflexivity_rule_attribute = Reflp_Preserve.add
+val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
 
 (* theory setup *)