equal
deleted
inserted
replaced
142 simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {* |
142 simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {* |
143 fn phi => fn ctxt => fn ct => |
143 fn phi => fn ctxt => fn ct => |
144 let |
144 let |
145 val dest = Thm.dest_comb; |
145 val dest = Thm.dest_comb; |
146 val f = (snd o dest o snd o dest) ct; |
146 val f = (snd o dest o snd o dest) ct; |
147 val [T, U] = Thm.dest_ctyp (ctyp_of_term f); |
147 val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_term f); |
148 val tr = instantiate' [SOME T, SOME U] [SOME f] |
148 val tr = instantiate' [SOME T, SOME U] [SOME f] |
149 (mk_meta_eq @{thm Abs_cfun_inverse2}); |
149 (mk_meta_eq @{thm Abs_cfun_inverse2}); |
150 val rules = Named_Theorems.get ctxt @{named_theorems cont2cont}; |
150 val rules = Named_Theorems.get ctxt @{named_theorems cont2cont}; |
151 val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules))); |
151 val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules))); |
152 in SOME (perhaps (SINGLE (tac 1)) tr) end |
152 in SOME (perhaps (SINGLE (tac 1)) tr) end |