src/HOL/HOLCF/Cfun.thy
changeset 59582 0fbed69ff081
parent 58957 c9e744ea8a38
child 59586 ddf6deaadfe8
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4      let
     1.5        val dest = Thm.dest_comb;
     1.6        val f = (snd o dest o snd o dest) ct;
     1.7 -      val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
     1.8 +      val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_term f);
     1.9        val tr = instantiate' [SOME T, SOME U] [SOME f]
    1.10            (mk_meta_eq @{thm Abs_cfun_inverse2});
    1.11        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};