--- a/Nominal/Ex/Lambda.thy	Thu Nov 03 13:19:23 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Mon Nov 07 13:58:18 2011 +0000
@@ -12,21 +12,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds 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 "local.frees_lst_graph"
- in 
-   Method.SIMPLE_METHOD' (K (all_tac))
- end)
-*}
-
-method_setup test = {* test *} {* test *}
-
 section {* Simple examples from Norrish 2004 *}
 
 nominal_primrec