diff -r a5e7ab090abf -r f7f1d8a98098 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Thu Oct 29 16:02:15 2009 +0100
+++ b/ProgTutorial/General.thy	Thu Oct 29 19:09:27 2009 +0100
@@ -1319,7 +1319,7 @@
   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 
   context (which we ignore in the code above) and a theorem (@{text thm}), and 
   returns another theorem (namely @{text thm} resolved with the theorem 
-  @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind "RS"} 
+  @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind RS in Drule} 
   is explained in Section~\ref{sec:simpletacs}). The function 
   @{ML rule_attribute in Thm} then returns  an attribute.