diff -r bc30e13b36a8 -r 914729515c26 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Fri Apr 23 16:38:22 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Fri Apr 23 17:01:36 1999 +0200
@@ -16,7 +16,7 @@
 
 text {|
   First we define a type abbreviation for binary operations over some
-  type @type "'val" of values.
+  type @{type "'val"} of values.
 |};
 
 types
@@ -98,7 +98,7 @@
 
 text {|
   The main result of this developement is the correctness theorem for
-  @term "comp".  We first establish some lemmas.
+  @{term "comp"}.  We first establish some lemmas.
 |};
 
 ML "reset HOL_quantifiers";