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