875 val concl = Logic.strip_imp_concl intro_t |
875 val concl = Logic.strip_imp_concl intro_t |
876 val (_, args) = strip_comb (HOLogic.dest_Trueprop concl) |
876 val (_, args) = strip_comb (HOLogic.dest_Trueprop concl) |
877 val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) |
877 val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) |
878 val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) |
878 val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) |
879 fun rewrite_pat (ct1, ct2) = |
879 fun rewrite_pat (ct1, ct2) = |
880 (ct1, Thm.cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2))) |
880 (ct1, Thm.global_cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2))) |
881 val t_insts' = map rewrite_pat t_insts |
881 val t_insts' = map rewrite_pat t_insts |
882 val intro'' = Thm.instantiate (T_insts, t_insts') intro |
882 val intro'' = Thm.instantiate (T_insts, t_insts') intro |
883 val [intro'''] = Variable.export ctxt3 ctxt [intro''] |
883 val [intro'''] = Variable.export ctxt3 ctxt [intro''] |
884 val intro'''' = |
884 val intro'''' = |
885 Simplifier.full_simplify |
885 Simplifier.full_simplify |