diff -r dacd47a0633f -r b4da1f2ec73f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Jul 25 16:46:53 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Jul 27 16:35:51 2013 +0200
@@ -666,17 +666,15 @@
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
       rewrite_goals_tac [pred_def] THEN
-      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
-      Tactic.compose_tac (false,
-        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_balanced (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness defs_ctxt t
-       (rewrite_goals_tac defs THEN
-        Tactic.compose_tac (false, ax, 0) 1));
+       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 in