src/HOL/Lifting.thy

--- a/src/HOL/Lifting.thy	Wed Dec 20 12:22:36 2017 +0100
+++ b/src/HOL/Lifting.thy	Wed Dec 20 14:53:34 2017 +0100
@@ -228,7 +228,7 @@
   fixes Abs :: "'a \<Rightarrow> 'b"
   and Rep :: "'b \<Rightarrow> 'a"
   assumes "type_definition Rep Abs (UNIV::'a set)"
-  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+  shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)"
 by (rule identity_equivp)
 
 lemma typedef_to_Quotient: