# HG changeset patch
# User haftmann
# Date 1150280082 -7200
# Node ID 1aad48bcc674e9797719fed1d1740502afdd7739
# Parent  2202a56488974e1ea66c8444578b748bc1d01077
slight adaption for code generator

diff -r 2202a5648897 -r 1aad48bcc674 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Datatype.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -257,14 +257,11 @@
   fst_conv [code]
   snd_conv [code]
 
-lemma [code unfolt]:
-  "1 == Suc 0" by simp
-
-code_syntax_tyco bool
+code_typapp bool
   ml (target_atom "bool")
   haskell (target_atom "Bool")
 
-code_syntax_const
+code_constapp
   True
     ml (target_atom "true")
     haskell (target_atom "True")
@@ -284,32 +281,32 @@
     ml (target_atom "(if __/ then __/ else __)")
     haskell (target_atom "(if __/ then __/ else __)")
 
-code_syntax_tyco
+code_typapp
   *
     ml (infix 2 "*")
     haskell (target_atom "(__,/ __)")
 
-code_syntax_const
+code_constapp
   Pair
     ml (target_atom "(__,/ __)")
     haskell (target_atom "(__,/ __)")
 
-code_syntax_tyco
+code_typapp
   unit
     ml (target_atom "unit")
     haskell (target_atom "()")
 
-code_syntax_const
+code_constapp
   Unity
     ml (target_atom "()")
     haskell (target_atom "()")
 
-code_syntax_tyco
+code_typapp
   option
     ml ("_ option")
     haskell ("Maybe _")
 
-code_syntax_const
+code_constapp
   None
     ml (target_atom "NONE")
     haskell (target_atom "Nothing")
diff -r 2202a5648897 -r 1aad48bcc674 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/HOL.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -1412,7 +1412,7 @@
   Not "HOL.not"
   arbitrary "HOL.arbitrary"
 
-code_syntax_const
+code_constapp
   "op =" (* an intermediate solution for polymorphic equality *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")
diff -r 2202a5648897 -r 1aad48bcc674 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -501,7 +501,7 @@
   arbitrary :: "'a"       ("(error \"arbitrary\")")
   arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
 
-code_syntax_const
+code_constapp
   "arbitrary :: 'a"       ml (target_atom "(error \"arbitrary\")")
   "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
 
diff -r 2202a5648897 -r 1aad48bcc674 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/List.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -2737,17 +2737,17 @@
   "List.op @" "List.append"
   "List.op mem" "List.mem"
 
-code_syntax_tyco
+code_typapp
   list
     ml ("_ list")
     haskell (target_atom "[_]")
 
-code_syntax_const
+code_constapp
   Nil
     ml (target_atom "[]")
     haskell (target_atom "[]")
 
-code_syntax_tyco
+code_typapp
   char
     ml (target_atom "char")
     haskell (target_atom "Char")
diff -r 2202a5648897 -r 1aad48bcc674 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -601,7 +601,8 @@
 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   by (induct m) simp_all
 
-lemma [code]: "Suc m + n = m + Suc n" by simp
+lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
+  by simp
 
 
 text {* Associative law for addition *}
diff -r 2202a5648897 -r 1aad48bcc674 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Wed Jun 14 12:14:13 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Wed Jun 14 12:14:42 2006 +0200
@@ -295,7 +295,7 @@
   CodegenPackage.add_appconst ("wfrec", ((3, 3), CodegenPackage.appgen_wfrec))
 *}
 
-code_syntax_const
+code_constapp
   wfrec
     ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;")
     haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x")