src/Pure/Isar/expression.ML
changeset 52732 b4da1f2ec73f
parent 52230 1105b3b5aa77
child 53041 d51bac27d4a0
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Jul 25 16:46:53 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Jul 27 16:35:51 2013 +0200
     1.3 @@ -666,17 +666,15 @@
     1.4  
     1.5      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
     1.6        rewrite_goals_tac [pred_def] THEN
     1.7 -      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
     1.8 -      Tactic.compose_tac (false,
     1.9 -        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    1.10 +      compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.11 +      compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    1.12  
    1.13      val conjuncts =
    1.14        (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
    1.15        |> Conjunction.elim_balanced (length ts);
    1.16      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    1.17        Element.prove_witness defs_ctxt t
    1.18 -       (rewrite_goals_tac defs THEN
    1.19 -        Tactic.compose_tac (false, ax, 0) 1));
    1.20 +       (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
    1.21    in ((statement, intro, axioms), defs_thy) end;
    1.22  
    1.23  in