--- a/CookBook/Recipes/NamedThms.thy	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Fri Jan 16 14:57:36 2009 +0000
@@ -48,9 +48,11 @@
 
 text {* and query the remaining ones with:
 
-@{ML_response_fake_both [display,gray] "thm foo" 
-"?C
-?B"}
+  \begin{isabelle}
+  \isacommand{thm}~@{text "foo"}\\
+  @{text "> ?C"}\\
+  @{text "> ?B"}\\
+  \end{isabelle}
 
   On the ML-level the rules marked with @{text "foo"} an be retrieved
   using the function @{ML FooRules.get}: