# HG changeset patch
# User desharna
# Date 1641846849 -3600
# Node ID e4fd3989554d8cf10e8fad5bab228111fa0d2340
# Parent  7733c794cfea98fc8c171c47dc1177f3ef9292f3# Parent  70aab133dc8dbd4ce6227aa9ee84d2e5a56ecf00
merged

diff -r 7733c794cfea -r e4fd3989554d src/HOL/Relation.thy
--- 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>
 
diff -r 7733c794cfea -r e4fd3989554d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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