--- a/src/HOL/ex/Refute_Examples.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Thu Nov 23 20:34:21 2006 +0100
@@ -480,11 +480,11 @@
subsection {* Inductive datatypes *}
-text {* With quick\_and\_dirty set, the datatype package does not generate
- certain axioms for recursion operators. Without these axioms, refute may
- find spurious countermodels. *}
+text {* With @{text quick_and_dirty} set, the datatype package does
+ not generate certain axioms for recursion operators. Without these
+ axioms, refute may find spurious countermodels. *}
-ML {* reset quick_and_dirty; *}
+ML {* reset quick_and_dirty *}
subsubsection {* unit *}