src/HOL/HOLCF/Cfun.thy
changeset 51717 9e7d1c139569
parent 49759 ecf1d5d87e5e
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -140,14 +140,14 @@
     1.4  *}
     1.5  
     1.6  simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {*
     1.7 -  fn phi => fn ss => fn ct =>
     1.8 +  fn phi => fn ctxt => fn ct =>
     1.9      let
    1.10        val dest = Thm.dest_comb;
    1.11        val f = (snd o dest o snd o dest) ct;
    1.12        val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
    1.13        val tr = instantiate' [SOME T, SOME U] [SOME f]
    1.14            (mk_meta_eq @{thm Abs_cfun_inverse2});
    1.15 -      val rules = Cont2ContData.get (Simplifier.the_context ss);
    1.16 +      val rules = Cont2ContData.get ctxt;
    1.17        val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
    1.18      in SOME (perhaps (SINGLE (tac 1)) tr) end
    1.19  *}