src/HOL/Tools/Lifting/lifting_setup.ML

           [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
         |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
           [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
         |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
           [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+          [reflp_thm])
       | NONE => lthy
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
           [quot_thm RS @{thm Quotient_All_transfer}])
         |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
           [quot_thm RS @{thm Quotient_Ex_transfer}])

           lthy'
             |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
               [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
             |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
               [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
+            |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+              [reflp_thm])
         end
       | _ => lthy'
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
           [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
         |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),