src/Tools/induct_tacs.ML
changeset 40722 441260986b63
parent 36960 01594f816e3a
child 42361 23f352990944
equal deleted inserted replaced
40721:e5089e903e39 40722:441260986b63
    94 
    94 
    95     val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
    95     val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
    96     val _ = Method.trace ctxt [rule'];
    96     val _ = Method.trace ctxt [rule'];
    97 
    97 
    98     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
    98     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
    99     val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    99     val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
   100       error "Induction rule has different numbers of variables";
   100       error "Induction rule has different numbers of variables";
   101   in res_inst_tac ctxt insts rule' i st end
   101   in res_inst_tac ctxt insts rule' i st end
   102   handle THM _ => Seq.empty;
   102   handle THM _ => Seq.empty;
   103 
   103 
   104 end;
   104 end;