src/HOL/Tools/datatype_package.ML
changeset 11725 d0c37d04906b
parent 11539 0f17da240450
child 11805 b110a1ea90da
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Oct 12 12:05:46 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 12 12:06:10 2001 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4    | prep_var _ = None;
     1.5  
     1.6  fun prep_inst (concl, xs) =	(*exception LIST*)
     1.7 -  let val vs = InductMethod.vars_of concl
     1.8 +  let val vs = InductAttrib.vars_of concl
     1.9    in mapfilter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.10  
    1.11  in
    1.12 @@ -199,7 +199,7 @@
    1.13            let val tn = find_tname (hd (mapfilter I (flat varss))) Bi
    1.14            in (#induction (datatype_info_sg_err sign tn), "Induction rule for type " ^ tn) end);
    1.15  
    1.16 -    val concls = InductMethod.concls_of rule;
    1.17 +    val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.18      val insts = flat (map prep_inst (concls ~~ varss)) handle LIST _ =>
    1.19        error (rule_name ^ " has different numbers of variables");
    1.20    in occs_in_prems (Tactic.res_inst_tac insts rule) (map #2 insts) i state end;