--- a/ProgTutorial/Package/Ind_Interface.thy	Mon Dec 31 20:20:55 2012 +0000
+++ b/ProgTutorial/Package/Ind_Interface.thy	Mon Feb 25 00:33:48 2013 +0000
@@ -161,7 +161,7 @@
   @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
 *}
 
-ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy =
+ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy =
 let
   val ((pred_specs', rule_specs'), _) = 
          Specification.read_spec pred_specs rule_specs lthy