src/HOL/Nominal/nominal_primrec.ML
changeset 23351 3702086a15a3
parent 23006 c46abff9a7a0
child 23418 c195f6f13769
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Jun 13 00:01:41 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Jun 13 00:01:51 2007 +0200
     1.3 @@ -372,9 +372,9 @@
     1.4             |> Theory.parent_path
     1.5           end))
     1.6        [goals] |>
     1.7 -    Proof.apply (Method.Basic (fn ctxt => Method.RAW_METHOD (fn ths =>
     1.8 +    Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
     1.9        rewrite_goals_tac (map snd defs_thms') THEN
    1.10 -      compose_tac (false, rule, length rule_prems) 1))) |>
    1.11 +      compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
    1.12      Seq.hd
    1.13    end;
    1.14