src/Pure/Isar/expression.ML
changeset 58956 a816aa3ff391
parent 57926 59b2572e8e93
child 59296 002d817b4c37
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Nov 09 11:05:20 2014 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Nov 09 14:08:00 2014 +0100
     1.3 @@ -683,8 +683,9 @@
     1.4      val intro = Goal.prove_global defs_thy [] norm_ts statement
     1.5        (fn {context = ctxt, ...} =>
     1.6          rewrite_goals_tac ctxt [pred_def] THEN
     1.7 -        compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
     1.8 -        compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
     1.9 +        compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    1.10 +        compose_tac defs_ctxt
    1.11 +          (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
    1.15 @@ -695,7 +696,7 @@
    1.16        |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
    1.17      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    1.18        Element.prove_witness axioms_ctxt t
    1.19 -       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
    1.20 +       (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
    1.21    in ((statement, intro, axioms), defs_thy) end;
    1.22  
    1.23  in