bugfix: induct_tac no longer raises THM "dest_state"
authorpaulson
Mon Jan 23 11:37:53 2006 +0100 (2006-01-23)
changeset 1875138dc4ff2a32b
parent 18750 91a328803c6a
child 18752 c9c6ae9e8b88
bugfix: induct_tac no longer raises THM "dest_state"
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jan 23 11:36:50 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jan 23 11:37:53 2006 +0100
     1.3 @@ -231,21 +231,22 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun gen_induct_tac inst_tac (varss, opt_rule) i state =
     1.8 +fun gen_induct_tac inst_tac (varss, opt_rule) i state = 
     1.9 +  SUBGOAL (fn (Bi,_) =>
    1.10    let
    1.11 -    val (_, _, Bi, _) = Thm.dest_state (state, i);
    1.12 -    val {sign, ...} = Thm.rep_thm state;
    1.13      val (rule, rule_name) =
    1.14 -      (case opt_rule of
    1.15 -        SOME r => (r, "Induction rule")
    1.16 -      | NONE =>
    1.17 -          let val tn = find_tname (hd (List.mapPartial I (List.concat varss))) Bi
    1.18 -          in (#induction (datatype_info_err sign tn), "Induction rule for type " ^ tn) end);
    1.19 -
    1.20 +      case opt_rule of
    1.21 +	  SOME r => (r, "Induction rule")
    1.22 +	| NONE =>
    1.23 +	    let val tn = find_tname (hd (List.mapPartial I (List.concat varss))) Bi
    1.24 +                val {sign, ...} = Thm.rep_thm state
    1.25 +	    in (#induction (datatype_info_err sign tn), "Induction rule for type " ^ tn) 
    1.26 +	    end
    1.27      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.28      val insts = List.concat (map prep_inst (concls ~~ varss)) handle UnequalLengths =>
    1.29        error (rule_name ^ " has different numbers of variables");
    1.30 -  in occs_in_prems (inst_tac insts rule) (map #2 insts) i state end;
    1.31 +  in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
    1.32 +  i state;
    1.33  
    1.34  fun induct_tac s =
    1.35    gen_induct_tac Tactic.res_inst_tac'