--- a/ProgTutorial/Package/Ind_Interface.thy	Wed Apr 29 00:36:14 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue May 05 03:21:49 2009 +0200
@@ -1,5 +1,5 @@
 theory Ind_Interface
-imports "../Base" "../Parsing" Simple_Inductive_Package
+imports "../Base" Simple_Inductive_Package
 begin
 
 section {* Parsing and Typing the Specification\label{sec:interface} *}
@@ -46,7 +46,7 @@
 \end{boxedminipage}
 \caption{Specification given by the user for the inductive predicates
 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and 
-@{text "fresh"}.\label{fig:specs}}
+@{term "fresh"}.\label{fig:specs}}
 \end{figure}  
 *}
 
@@ -120,7 +120,9 @@
   accpart'
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
-
+(*<*)ML %no{*fun filtered_input str = 
+  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 
+fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*)
 text {*
   Note that in these definitions the parameter @{text R}, standing for the
   relation, is left implicit. For the moment we will ignore this kind
@@ -152,19 +154,17 @@
   done in Lines 5 to 7 in the code below.
 *}
 
-(*<*)ML %linenos{*fun add_inductive pred_specs rule_specs lthy = lthy 
-fun add_inductive_cmd pred_specs rule_specs lthy =
-let
-  val ((pred_specs', rule_specs'), _) = 
-         Specification.read_spec pred_specs rule_specs lthy
-in
-  add_inductive pred_specs' rule_specs' lthy
-end*}(*>*)
+(*<*)
+ML %linenos 
+{* 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)
 
-val _ = OuterSyntax.local_theory "simple_inductive" 
+val _ = OuterSyntax.local_theory "simple_inductive2" 
           "definition of simple inductive predicates"
              OuterKeyword.thy_decl specification*}
 
@@ -191,7 +191,7 @@
   @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
 *}
 
-ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
+ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy =
 let
   val ((pred_specs', rule_specs'), _) = 
          Specification.read_spec pred_specs rule_specs lthy
@@ -199,11 +199,9 @@
   add_inductive pred_specs' rule_specs' lthy
 end*}
 
-ML {* Specification.read_spec *}
-
 text {*
   Once we have the input data as some internal datastructure, we call
-  the function @{ML add_inductive}. This function does the  heavy duty 
+  the function @{text add_inductive}. This function does the  heavy duty 
   lifting in the package: it generates definitions for the 
   predicates and derives from them corresponding induction principles and 
   introduction rules. The description of this function will span over