# HG changeset patch
# User desharna
# Date 1665421674 -7200
# Node ID 207b6fcfc47df9b0b74a76016783df414542fd33
# Parent  b3ff4f171edaa847525ac40e864e9169fbe4bf9a
removed unused universal variable from lemma reflp_onI

diff -r b3ff4f171eda -r 207b6fcfc47d src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Oct 10 13:42:14 2022 +0200
+++ b/src/HOL/Relation.thy	Mon Oct 10 19:07:54 2022 +0200
@@ -173,7 +173,7 @@
   unfolding refl_on_def by (iprover intro!: ballI)
 
 lemma reflp_onI:
-  "(\<And>x y. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
+  "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
   by (simp add: reflp_on_def)
 
 lemma reflpI[intro?]: "(\<And>x. R x x) \<Longrightarrow> reflp R"