--- a/ProgTutorial/Package/Ind_Interface.thy	Tue May 05 03:21:49 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Fri May 08 17:11:57 2009 +0200
@@ -151,15 +151,11 @@
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we
   need for calling the package and setting up the keyword. The latter is
-  done in Lines 5 to 7 in the code below.
+  done in Lines 5 to 7 in the code below.\footnote{FIXME: Is there a way to state 
+  here @{text "simple_inductive"}?}
 *}
-
-(*<*)
-ML %linenos 
-{* fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
-   fun add_inductive pred_specs rule_specs lthy = lthy *}
-(*>*)
-
+(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
+   fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)
 ML_val %linenosgray{*val specification =
   spec_parser >>
     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)