equal
deleted
inserted
replaced
60 |
60 |
61 fun is_nat t = (fastype_of1 t = HOLogic.natT); |
61 fun is_nat t = (fastype_of1 t = HOLogic.natT); |
62 |
62 |
63 fun mk_nat_thm thy t = |
63 fun mk_nat_thm thy t = |
64 let |
64 let |
65 val cn = Thm.cterm_of thy (Var (("n", 0), HOLogic.natT)) |
65 val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT)) |
66 and ct = Thm.cterm_of thy t |
66 and ct = Thm.global_cterm_of thy t |
67 in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end; |
67 in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end; |
68 |
68 |
69 end; |
69 end; |
70 |
70 |
71 |
71 |