--- a/src/HOL/Groups.thy Wed Apr 06 13:33:46 2011 +0200
+++ b/src/HOL/Groups.thy Wed Apr 06 14:08:40 2011 +0200
@@ -130,7 +130,9 @@
if not (null ts) orelse T = dummyT
orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
then raise Match
- else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ ctxt T);
+ else
+ Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
+ Syntax_Phases.term_of_typ ctxt T);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
*} -- {* show types that are presumably too general *}