Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Lambda.thy
changeset 2169 61a89e41c55b
parent 2162 d76667e51d30
child 2170 1fe84fd8f8a4 
--- a/Nominal/Ex/Lambda.thy	Fri May 21 10:42:53 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri May 21 10:43:14 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)
nominal2