equal
deleted
inserted
replaced
48 *} |
48 *} |
49 |
49 |
50 setup {* |
50 setup {* |
51 let |
51 let |
52 |
52 |
53 fun remove_suc thy thms = |
53 fun remove_suc ctxt thms = |
54 let |
54 let |
|
55 val thy = Proof_Context.theory_of ctxt; |
55 val vname = singleton (Name.variant_list (map fst |
56 val vname = singleton (Name.variant_list (map fst |
56 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
57 (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
57 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
58 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
58 fun lhs_of th = snd (Thm.dest_comb |
59 fun lhs_of th = snd (Thm.dest_comb |
59 (fst (Thm.dest_comb (cprop_of th)))); |
60 (fst (Thm.dest_comb (cprop_of th)))); |