src/HOL/List.thy
changeset 19890 1aad48bcc674
parent 19817 bb16bf9ae3fd
child 20044 92cc2f4c7335
--- 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")