--- a/Nominal/Ex/Lambda.thy	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 22 12:18:22 2011 +0100
@@ -3,6 +3,7 @@
 begin
 
 
+
 atom_decl name
 
 nominal_datatype lam =
@@ -10,11 +11,27 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+ML {* Method.SIMPLE_METHOD' *}
+ML {* Sign.intern_const *}
+
+ML {*
+val test:((Proof.context -> Method.method) context_parser) =
+Scan.succeed (fn ctxt =>
+ let
+   val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph"
+ in 
+   Method.SIMPLE_METHOD' (K all_tac)
+ end)
+*}
+
+method_setup test = {* test *} {* test *}
 
 section {* free name function *}
 
 text {* first returns an atom list *}
 
+ML Thm.implies_intr
+
 nominal_primrec 
   frees_lst :: "lam \<Rightarrow> atom list"
 where