--- a/src/Doc/IsarImplementation/ML.thy Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Sun Mar 02 19:00:45 2014 +0100
@@ -1439,8 +1439,8 @@
Literal integers in ML text are forced to be of this one true
integer type --- adhoc overloading of SML97 is disabled.
- Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
- @{ML_struct Int}. Structure @{ML_struct Integer} in @{file
+ Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
+ @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
"~~/src/Pure/General/integer.ML"} provides some additional
operations.
@@ -1487,7 +1487,7 @@
*}
text {* Apart from @{ML Option.map} most other operations defined in
- structure @{ML_struct Option} are alien to Isabelle/ML an never
+ structure @{ML_structure Option} are alien to Isabelle/ML an never
used. The operations shown above are defined in @{file
"~~/src/Pure/General/basics.ML"}. *}