changeset 62178 | c3c98ed94b0f |
parent 61841 | 4d3527b94f2a |
--- a/src/HOL/Nominal/nominal_induct.ML Wed Jan 13 23:37:55 2016 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Thu Jan 14 12:11:22 2016 +0100 @@ -165,7 +165,7 @@ in -val nominal_induct_method = +val nominal_induct_method : (Proof.context -> Proof.method) context_parser = Scan.lift (Args.mode Induct.no_simpN) -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- avoiding -- fixing -- rule_spec) >>