--- a/ProgTutorial/Package/Ind_Interface.thy Mon May 24 20:02:11 2010 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy Thu May 27 10:39:07 2010 +0200
@@ -61,12 +61,12 @@
*}
ML{*val spec_parser =
- OuterParse.fixes --
+ Parse.fixes --
Scan.optional
- (OuterParse.$$$ "where" |--
- OuterParse.!!!
- (OuterParse.enum1 "|"
- (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+ (Parse.$$$ "where" |--
+ Parse.!!!
+ (Parse.enum1 "|"
+ (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*}
text {*
which we explained in Section~\ref{sec:parsingspecs}. There is no code included
@@ -95,8 +95,8 @@
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*}(*>*)
+ filter Token.is_proper (Outer_Syntax.scan Position.none str)
+fun parse p input = Scan.finite Token.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
@@ -133,13 +133,13 @@
spec_parser >>
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
-val _ = OuterSyntax.local_theory "simple_inductive2"
+val _ = Outer_Syntax.local_theory "simple_inductive2"
"definition of simple inductive predicates"
- OuterKeyword.thy_decl specification*}
+ Keyword.thy_decl specification*}
text {*
- We call @{ML_ind local_theory in OuterSyntax} with the kind-indicator
- @{ML_ind thy_decl in OuterKeyword} since the package does not need to open
+ We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator
+ @{ML_ind thy_decl in Keyword} since the package does not need to open
up any proof (see Section~\ref{sec:newcommand}).
The auxiliary function @{text specification} in Lines 1 to 3
gathers the information from the parser to be processed further