equal
deleted
inserted
replaced
177 val tn = find_tname (hd vars) Bi; |
177 val tn = find_tname (hd vars) Bi; |
178 val {induction, ...} = datatype_info_sg_err sign tn; |
178 val {induction, ...} = datatype_info_sg_err sign tn; |
179 val ind_vnames = map (fn (_ $ Var (ixn, _)) => |
179 val ind_vnames = map (fn (_ $ Var (ixn, _)) => |
180 implode (tl (explode (Syntax.string_of_vname ixn)))) |
180 implode (tl (explode (Syntax.string_of_vname ixn)))) |
181 (dest_conj (HOLogic.dest_Trueprop (concl_of induction))); |
181 (dest_conj (HOLogic.dest_Trueprop (concl_of induction))); |
182 val insts = (ind_vnames ~~ vars) handle _ => |
182 val insts = (ind_vnames ~~ vars) handle LIST _ => |
183 error ("Induction rule for type " ^ tn ^ " has different number of variables") |
183 error ("Induction rule for type " ^ tn ^ " has different number of variables") |
184 in |
184 in |
185 occs_in_prems (res_inst_tac insts induction) vars i state |
185 occs_in_prems (res_inst_tac insts induction) vars i state |
186 end; |
186 end; |
187 |
187 |