diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Wed Jan 25 21:10:54 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Wed Jan 25 21:14:00 2012 +0100
@@ -356,7 +356,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type term} \\
-  @{index_ML "op aconv": "term * term -> bool"} \\
+  @{index_ML_op "aconv": "term * term -> bool"} \\
   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
@@ -380,7 +380,7 @@
   \item Type @{ML_type term} represents de-Bruijn terms, with comments
   in abstractions, and explicitly named free variables and constants;
   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
-  Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
+  Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.
 
   \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
@@ -700,7 +700,7 @@
   \item @{ML Thm.capply}, @{ML Thm.cabs}, @{ML Thm.all}, @{ML
   Drule.mk_implies} etc.\ compose certified terms (or propositions)
   incrementally.  This is equivalent to @{ML Thm.cterm_of} after
-  unchecked @{ML "op $"}, @{ML lambda}, @{ML Logic.all}, @{ML
+  unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML
   Logic.mk_implies} etc., but there can be a big difference in
   performance when large existing entities are composed by a few extra
   constructions on top.  There are separate operations to decompose
@@ -1084,14 +1084,14 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML "op RSN": "thm * (int * thm) -> thm"} \\
-  @{index_ML "op RS": "thm * thm -> thm"} \\
+  @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
+  @{index_ML_op "RS": "thm * thm -> thm"} \\
 
-  @{index_ML "op RLN": "thm list * (int * thm list) -> thm list"} \\
-  @{index_ML "op RL": "thm list * thm list -> thm list"} \\
+  @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
+  @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
 
-  @{index_ML "op MRS": "thm list * thm -> thm"} \\
-  @{index_ML "op OF": "thm * thm list -> thm"} \\
+  @{index_ML_op "MRS": "thm list * thm -> thm"} \\
+  @{index_ML_op "OF": "thm * thm list -> thm"} \\
   \end{mldecls}
 
   \begin{description}