src/HOL/HOLCF/ex/Pattern_Match.thy
changeset 54742 7a86358a3c0b
parent 52143 36ffe23b25f8
child 54895 515630483010
     1.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -411,8 +411,8 @@
     1.4      : thm =
     1.5    let
     1.6      fun tac {prems, context} =
     1.7 -      rewrite_goals_tac defs THEN
     1.8 -      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
     1.9 +      rewrite_goals_tac context defs THEN
    1.10 +      EVERY (tacs {prems = map (rewrite_rule context defs) prems, context = context})
    1.11    in
    1.12      Goal.prove_global thy [] [] goal tac
    1.13    end;