equal
deleted
inserted
replaced
171 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms; |
171 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms; |
172 |
172 |
173 in |
173 in |
174 |
174 |
175 val nominal_induct_method = |
175 val nominal_induct_method = |
176 Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- |
176 Scan.lift (Args.mode Induct.no_simpN) -- |
177 avoiding -- fixing -- rule_spec) >> |
177 (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) -- |
|
178 avoiding -- fixing -- rule_spec) >> |
178 (fn (no_simp, (((x, y), z), w)) => fn ctxt => |
179 (fn (no_simp, (((x, y), z), w)) => fn ctxt => |
179 RAW_METHOD_CASES (fn facts => |
180 RAW_METHOD_CASES (fn facts => |
180 HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); |
181 HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); |
181 |
182 |
182 end |
183 end |