# HG changeset patch
# User wenzelm
# Date 1159386574 -7200
# Node ID c8fdad2dc6e6798820c5bcd3fe6edc62405e861c
# Parent  5a103b43da5ad7f0e1ac70589628e7352a592096
proper const_syntax for uminus, abs;

diff -r 5a103b43da5a -r c8fdad2dc6e6 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 27 21:44:38 2006 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 27 21:49:34 2006 +0200
@@ -229,13 +229,13 @@
 end;
 *} -- {* show types that are presumably too general *}
 
-syntax
-  uminus :: "'a\<Colon>minus \<Rightarrow> 'a" ("- _" [81] 80)
+const_syntax
+  uminus  ("- _" [81] 80)
 
-syntax (xsymbols)
-  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
-syntax (HTML output)
-  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
+const_syntax (xsymbols)
+  abs  ("\<bar>_\<bar>")
+const_syntax (HTML output)
+  abs  ("\<bar>_\<bar>")
 
 
 subsection {*Equality*}