diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Groups.thy --- 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 \ \ \show types that are presumably too general\ class plus =