fixed Method.Basic;
authorwenzelm
Sat, 25 Jul 2009 18:55:30 +0200
changeset 32196 bda40fb76a65
parent 32195 d77476e4040c
child 32197 bc341bbe4417
child 32207 d64a1820431d
fixed Method.Basic;
src/HOL/Nominal/nominal_primrec.ML
--- 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;