changeset 2891 | 304dfe6cc83a |
parent 2885 | 1264f2a21ea9 |
child 2902 | 9c3f6a4d95d4 |
--- 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)