--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Mon Dec 06 01:05:58 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Mon Dec 06 01:06:22 2004 +0100
@@ -245,7 +245,7 @@
You can simulate this in Isabelle by instantiating the @{term xs} in
definition \mbox{@{thm hd.simps[no_vars]}} with a constant @{text DUMMY} that
is printed as @{term DUMMY}. The code for the pattern above is
- \verb!@!\verb!{thm hd.simps [where xs=DUMMY,novars]}!.
+ \verb!@!\verb!{thm hd.simps [where xs=DUMMY,no_vars]}!.
You can drive this game even further and extend the syntax of let
bindings such that certain functions like @{term fst}, @{term hd},