--- a/CookBook/FirstSteps.thy	Thu Jan 29 17:09:56 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Jan 29 17:10:13 2009 +0000
@@ -522,7 +522,21 @@
 
 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
 
-  authentic syntax
+  authentic syntax?
+
+*}
+
+ML {* @{const_name lfp} *}
+
+text {*
+  constants in case-patterns?
+
+  In the meantime, lfp has been moved to the Inductive theory, so it is  
+  no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been  
+  used, we would have gotten an error for this. Another advantage of the  
+  antiquotation is that we can then just write @{text "@{const_name lfp}"} rather  
+  than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct  
+  name.
   
 *}
 
@@ -719,4 +733,8 @@
 thm foo_def
 (*>*)
 
+section {* Misc *}
+
+ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
+
 end
\ No newline at end of file