--- a/src/HOL/Relation.thy Mon Jan 10 14:05:33 2022 +0100
+++ b/src/HOL/Relation.thy Mon Jan 10 21:34:09 2022 +0100
@@ -261,19 +261,18 @@
lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
by (simp add: asym.simps)
+lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
+ by (rule asymD[to_pred])
+
lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
by (blast intro: asymI dest: asymD)
-context preorder begin
-
-lemma asymp_less[simp]: "asymp (<)"
+lemma (in preorder) asymp_less[simp]: "asymp (<)"
by (auto intro: asympI dual_order.asym)
-lemma asymp_greater[simp]: "asymp (>)"
+lemma (in preorder) asymp_greater[simp]: "asymp (>)"
by (auto intro: asympI dual_order.asym)
-end
-
subsubsection \<open>Symmetry\<close>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jan 10 14:05:33 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jan 10 21:34:09 2022 +0100
@@ -392,7 +392,7 @@
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
let
fun varify_noninducts (t as Free (s, T)) =
- if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
+ if (s, T) = ind_x then t else Var ((s, 0), T)
| varify_noninducts t = t
val p_inst = concl_prop