# HG changeset patch
# User berghofe
# Date 1178804971 -7200
# Node ID 66baa75eae06f252e7ec805358b3be18ec859131
# Parent  475ff421a6a34b214815a323788a5a8570aa6485
Name of ML function "not" is now qualified in order to avoid
clashes with names of constants introduced by the user.

diff -r 475ff421a6a3 -r 66baa75eae06 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Thu May 10 10:22:17 2007 +0200
+++ b/src/HOL/Code_Generator.thy	Thu May 10 15:49:31 2007 +0200
@@ -36,7 +36,7 @@
   "Trueprop" ("(_)")
   "True"    ("true")
   "False"   ("false")
-  "Not"     ("not")
+  "Not"     ("Bool.not")
   "op |"    ("(_ orelse/ _)")
   "op &"    ("(_ andalso/ _)")
   "If"      ("(if _/ then _/ else _)")