--- a/Nominal/Ex/Lambda.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/Lambda.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -19,6 +19,37 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
+ML {*
+  Outer_Syntax.local_theory_to_proof;
+  Proof.theorem
+*}
+
+ML {*
+fun prove_strong_ind pred_name avoids ctxt =
+  let
+    val _ = ()
+  in
+    Proof.theorem NONE (fn thss => fn ctxt => ctxt) [] ctxt
+  end
+
+(* outer syntax *)
+local
+  structure P = Parse;
+  structure S = Scan
+
+in
+val _ =
+  Outer_Syntax.local_theory_to_proof "nominal_inductive"
+    "prove strong induction theorem for inductive predicate involving nominal datatypes"
+    Keyword.thy_goal
+    (Parse.xname -- 
+     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
+      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn (pred_name, avoids) =>
+        prove_strong_ind pred_name avoids))
+
+end
+*}
+
 
 section {* Typing *}
 
@@ -27,9 +58,6 @@
 | TFun ty ty ("_ \<rightarrow> _") 
 
 
-(*
-declare ty.perm[eqvt]
-
 inductive
   valid :: "(name \<times> ty) list \<Rightarrow> bool"
 where
@@ -53,6 +81,7 @@
 
 thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
 
+(*
 lemma
   fixes c::"'a::fs"
   assumes a: "\<Gamma> \<turnstile> t : T"