src/HOL/Groups.thy
changeset 69216 1a52baa70aed
parent 64290 fb5c74a58796
child 69593 3dda49e08b9d
--- a/src/HOL/Groups.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Groups.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -182,7 +182,7 @@
         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
           Syntax_Phases.term_of_typ ctxt T
       else raise Match);
-  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
+  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end
 \<close> \<comment> \<open>show types that are presumably too general\<close>
 
 class plus =