diff -r 503630c553a8 -r 304dfe6cc83a Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Jun 23 13:09:17 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Thu Jun 23 22:21:43 2011 +0100 @@ -18,7 +18,7 @@ val test:((Proof.context -> Method.method) context_parser) = Scan.succeed (fn ctxt => let - val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph" + val _ = Inductive.the_inductive ctxt "local.frees_lst_graph" in Method.SIMPLE_METHOD' (K all_tac) end)