src/HOL/HOL.thy

 in
   map (tr' o prefix Syntax.constN) ["HOL.one", "HOL.zero"]
 end;
 *} -- {* show types that are presumably too general *}
 
-syntax
-  uminus :: "'a\<Colon>minus \<Rightarrow> 'a" ("- _" [81] 80)
-
-syntax (xsymbols)
-  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
-syntax (HTML output)
-  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
+const_syntax
+  uminus  ("- _" [81] 80)
+
+const_syntax (xsymbols)
+  abs  ("\<bar>_\<bar>")
+const_syntax (HTML output)
+  abs  ("\<bar>_\<bar>")
 
 
 subsection {*Equality*}
 
 lemma sym: "s = t ==> t = s"