src/HOL/HOLCF/Cfun.thy
changeset 58957 c9e744ea8a38
parent 58880 0baae4311a9f
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4        val tr = instantiate' [SOME T, SOME U] [SOME f]
     1.5            (mk_meta_eq @{thm Abs_cfun_inverse2});
     1.6        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
     1.7 -      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
     1.8 +      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
     1.9      in SOME (perhaps (SINGLE (tac 1)) tr) end
    1.10  *}
    1.11