author | wenzelm |
Thu, 14 Jan 2016 12:11:22 +0100 | |
changeset 62178 | c3c98ed94b0f |
parent 62177 | 3a578ee55bff |
child 62179 | e089e5b02443 |
--- 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) >>