changeset 20328 | 5b240a4216b0 |
parent 20218 | be3bfb0699ba |
child 20597 | 65fe827aa595 |
--- a/src/HOL/Tools/datatype_package.ML Thu Aug 03 15:58:04 2006 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Aug 03 17:30:36 2006 +0200 @@ -247,7 +247,7 @@ val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name)))); -val inst_tac = Method.bires_inst_tac false; +val inst_tac = RuleInsts.bires_inst_tac false; fun induct_meth ctxt (varss, opt_rule) = gen_induct_tac (inst_tac ctxt) (varss, opt_rule);