src/HOL/Nominal/nominal_primrec.ML
changeset 54742 7a86358a3c0b
parent 46961 5c6955f487e5
child 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -373,8 +373,8 @@
     1.4            |> snd
     1.5          end)
     1.6        [goals] |>
     1.7 -    Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
     1.8 -      rewrite_goals_tac defs_thms THEN
     1.9 +    Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
    1.10 +      rewrite_goals_tac ctxt defs_thms THEN
    1.11        compose_tac (false, rule, length rule_prems) 1))) |>
    1.12      Seq.hd
    1.13    end;