equal
deleted
inserted
replaced
16 |
16 |
17 ML {* |
17 ML {* |
18 val test:((Proof.context -> Method.method) context_parser) = |
18 val test:((Proof.context -> Method.method) context_parser) = |
19 Scan.succeed (fn ctxt => |
19 Scan.succeed (fn ctxt => |
20 let |
20 let |
21 val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph" |
21 val _ = Inductive.the_inductive ctxt "local.frees_lst_graph" |
22 in |
22 in |
23 Method.SIMPLE_METHOD' (K all_tac) |
23 Method.SIMPLE_METHOD' (K all_tac) |
24 end) |
24 end) |
25 *} |
25 *} |
26 |
26 |