--- a/Nominal/Ex/Lambda.thy	Fri May 21 10:47:07 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri May 21 10:47:45 2010 +0200
@@ -456,10 +456,10 @@
 fun prove_strong_ind (pred_name, avoids) ctxt = 
   Proof.theorem NONE (K I) [] ctxt
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.local_theory_to_proof "nominal_inductive"
+  Outer_Syntax.local_theory_to_proof "nominal_inductive"
     "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
       (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
         (P.$$$ ":" |-- P.and_list1 P.term))) []) >>  prove_strong_ind)