diff -r 667a0943c40b -r 4e3f262a459d CookBook/FirstSteps.thy --- 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