# HG changeset patch
# User wenzelm
# Date 1154619036 -7200
# Node ID 5b240a4216b0323faf917370f43d23fc0fbfc622
# Parent  69a9d839dcc8ed22e5b387bf61e360fe1dfd4d9c
RuleInsts.bires_inst_tac;

diff -r 69a9d839dcc8 -r 5b240a4216b0 src/HOL/Tools/datatype_package.ML
--- 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);