src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Mon Sep 23 17:15:44 2019 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 24 12:56:10 2019 +0100
@@ -1177,7 +1177,7 @@
 lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r"
   by (simp add: acyclic_def)
 
-lemma (in order) acyclicI_order:
+lemma (in preorder) acyclicI_order:
   assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a"
   shows "acyclic r"
 proof -