equal
deleted
inserted
replaced
492 (*instantiate the variable to a tuple, if it is non-trivial, in order to |
492 (*instantiate the variable to a tuple, if it is non-trivial, in order to |
493 allow the predicate to be "opened up". |
493 allow the predicate to be "opened up". |
494 The name "x.1" comes from the "RS spec" !*) |
494 The name "x.1" comes from the "RS spec" !*) |
495 val inst = |
495 val inst = |
496 case elem_frees of [_] => I |
496 case elem_frees of [_] => I |
497 | _ => Drule.instantiate_normalize ([], [(Thm.cterm_of thy (Var(("x",1), Ind_Syntax.iT)), |
497 | _ => Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy (Var(("x",1), Ind_Syntax.iT)), |
498 Thm.cterm_of thy elem_tuple)]); |
498 Thm.global_cterm_of thy elem_tuple)]); |
499 |
499 |
500 (*strip quantifier and the implication*) |
500 (*strip quantifier and the implication*) |
501 val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp})); |
501 val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp})); |
502 |
502 |
503 val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = Thm.concl_of induct0 |
503 val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = Thm.concl_of induct0 |