# HG changeset patch
# User haftmann
# Date 1138021672 -3600
# Node ID f0d901bc0686780199b1f87407ad33b9c28aea59
# Parent  5eb3df798405f678471f55ab725312e5fbb1c5a3
removed problematic keyword 'atom'

diff -r 5eb3df798405 -r f0d901bc0686 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Jan 23 14:06:40 2006 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Jan 23 14:07:52 2006 +0100
@@ -202,14 +202,12 @@
   '("advanced"
     "and"
     "assumes"
-    "atom"
     "attach"
     "begin"
     "binder"
     "case_eqns"
     "con_defs"
     "concl"
-    "constants"
     "constrains"
     "contains"
     "defines"
@@ -236,6 +234,7 @@
     "recursor_eqns"
     "shows"
     "structure"
+    "target_atom"
     "type_elims"
     "type_intros"
     "uses"
diff -r 5eb3df798405 -r f0d901bc0686 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Jan 23 14:06:40 2006 +0100
+++ b/etc/isar-keywords.el	Mon Jan 23 14:07:52 2006 +0100
@@ -217,14 +217,12 @@
     "advanced"
     "and"
     "assumes"
-    "atom"
     "attach"
     "begin"
     "binder"
     "compose"
     "concl"
     "congs"
-    "constants"
     "constrains"
     "contains"
     "defines"
@@ -265,6 +263,7 @@
     "signature"
     "states"
     "structure"
+    "target_atom"
     "to"
     "transitions"
     "transrel"
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Datatype.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -224,16 +224,16 @@
 
 code_syntax_const
   True
-    ml (atom "true")
-    haskell (atom "True")
+    ml (target_atom "true")
+    haskell (target_atom "True")
   False
-    ml (atom "false")
-    haskell (atom "False")
+    ml (target_atom "false")
+    haskell (target_atom "False")
 
 code_syntax_const
   Pair
-    ml (atom "(__,/ __)")
-    haskell (atom "(__,/ __)")
+    ml (target_atom "(__,/ __)")
+    haskell (target_atom "(__,/ __)")
 
 code_syntax_const
   1 :: "nat"
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/HOL.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -1377,13 +1377,13 @@
   uminus "HOL.uminus"
 
 code_syntax_tyco bool
-  ml (atom "bool")
-  haskell (atom "Bool")
+  ml (target_atom "bool")
+  haskell (target_atom "Bool")
 
 code_syntax_const
   Not
-    ml (atom "not")
-    haskell (atom "not")
+    ml (target_atom "not")
+    haskell (target_atom "not")
   "op &"
     ml (infixl 1 "andalso")
     haskell (infixl 3 "&&")
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -897,16 +897,16 @@
   "neg"                         ("(_ < 0)")
 
 code_syntax_tyco int
-  ml (atom "IntInf.int")
-  haskell (atom "Integer")
+  ml (target_atom "IntInf.int")
+  haskell (target_atom "Integer")
 
 code_syntax_const
   0 :: "int"
-    ml (atom "(0:IntInf.int)")
-    haskell (atom "0")
+    ml (target_atom "(0:IntInf.int)")
+    haskell (target_atom "0")
   1 :: "int"
-    ml (atom "(1:IntInf.int)")
-    haskell (atom "1")
+    ml (target_atom "(1:IntInf.int)")
+    haskell (target_atom "1")
   "op +" :: "int \<Rightarrow> int \<Rightarrow> int"
     ml (infixl 8 "+")
     haskell (infixl 6 "+")
@@ -914,8 +914,8 @@
     ml (infixl 9 "*")
     haskell (infixl 7 "*")
   uminus :: "int \<Rightarrow> int"
-    ml (atom "~")
-    haskell (atom "negate")
+    ml (target_atom "~")
+    haskell (target_atom "negate")
   "op <" :: "int \<Rightarrow> int \<Rightarrow> bool"
     ml (infix 6 "<")
     haskell (infix 4 "<")
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -52,12 +52,12 @@
   int ("(_)")
 
 (* code_syntax_tyco nat
-  ml (atom "InfInt.int")
-  haskell (atom "Integer")
+  ml (target_atom "InfInt.int")
+  haskell (target_atom "Integer")
 
 code_syntax_const 0 :: nat
   ml ("0 : InfInt.int")
-  haskell (atom "0")
+  haskell (target_atom "0")
 
 code_syntax_const Suc
   ml (infixl 8 "_ + 1")
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -29,11 +29,11 @@
 
 code_syntax_tyco set
   ml ("_ list")
-  haskell (atom "[_]")
+  haskell (target_atom "[_]")
 
 code_syntax_const "{}"
-  ml (atom "[]")
-  haskell (atom "[]")
+  ml (target_atom "[]")
+  haskell (target_atom "[]")
 
 consts_code
   "{}"      ("[]")
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/List.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -2694,12 +2694,12 @@
 code_syntax_tyco
   list
     ml ("_ list")
-    haskell (atom "[_]")
+    haskell (target_atom "[_]")
 
 code_syntax_const
   Nil
-    ml (atom "[]")
-    haskell (atom "[]")
+    ml (target_atom "[]")
+    haskell (target_atom "[]")
 
 setup list_codegen_setup
 
diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Product_Type.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -798,13 +798,13 @@
 code_syntax_tyco
   *
     ml (infix 2 "*")
-    haskell (atom "(__,/ __)")
+    haskell (target_atom "(__,/ __)")
 
 code_syntax_const
   fst
-    haskell (atom "fst")
+    haskell (target_atom "fst")
   snd
-    haskell (atom "snd")
+    haskell (target_atom "snd")
 
 ML {*