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