--- a/src/HOL/Enum.thy Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Enum.thy Mon Sep 24 14:30:09 2018 +0200
@@ -585,7 +585,7 @@
definition [simp]: "Groups.zero = a\<^sub>1"
definition [simp]: "Groups.one = a\<^sub>1"
definition [simp]: "(+) = (\<lambda>_ _. a\<^sub>1)"
-definition [simp]: "( * ) = (\<lambda>_ _. a\<^sub>1)"
+definition [simp]: "(*) = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "(mod) = (\<lambda>_ _. a\<^sub>1)"
definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
@@ -690,7 +690,7 @@
definition "(-) = ((+) :: finite_2 \<Rightarrow> _)"
definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_2. x)"
-definition "divide = (( * ) :: finite_2 \<Rightarrow> _)"
+definition "divide = ((*) :: finite_2 \<Rightarrow> _)"
definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "abs = (\<lambda>x :: finite_2. x)"
definition "sgn = (\<lambda>x :: finite_2. x)"