changeset 57945 | cacb00a569e0 |
parent 52143 | 36ffe23b25f8 |
child 57954 | c52223cd1003 |
--- a/src/HOL/HOLCF/Cfun.thy Fri Aug 15 18:02:34 2014 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Sat Aug 16 11:35:33 2014 +0200 @@ -147,7 +147,7 @@ val [T, U] = Thm.dest_ctyp (ctyp_of_term f); val tr = instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2}); - val rules = Cont2ContData.get ctxt; + val rules = Named_Theorems.get ctxt @{named_theorems cont2cont}; val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)); in SOME (perhaps (SINGLE (tac 1)) tr) end *}