author | wenzelm |
Sat, 25 Jul 2009 18:55:30 +0200 | |
changeset 32196 | bda40fb76a65 |
parent 32195 | d77476e4040c |
child 32197 | bc341bbe4417 |
child 32207 | d64a1820431d |
--- a/src/HOL/Nominal/nominal_primrec.ML Sat Jul 25 18:55:12 2009 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Jul 25 18:55:30 2009 +0200 @@ -380,7 +380,7 @@ [goals] |> Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ => rewrite_goals_tac defs_thms THEN - compose_tac (false, rule, length rule_prems) 1)) |> + compose_tac (false, rule, length rule_prems) 1))) |> Seq.hd end;