src/HOL/Tools/Lifting/lifting_setup.ML

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue May 31 20:56:09 2022 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Jun 04 15:43:34 2022 +0200
@@ -758,7 +758,7 @@
           handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
       in
         case reflp_tm of
-          Const (\<^const_name>\<open>reflp\<close>, _) $ _ => ()
+          \<^Const_>\<open>reflp_on _ for \<^Const>\<open>top_class.top _\<close> _\<close> => ()
           | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
       end