src/Pure/Isar/expression.ML
changeset 52230 1105b3b5aa77
parent 52153 f5773a46cf05
child 52732 b4da1f2ec73f
     1.1 --- a/src/Pure/Isar/expression.ML	Thu May 30 08:27:51 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu May 30 12:35:40 2013 +0200
     1.3 @@ -671,8 +671,7 @@
     1.4          Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
     1.5  
     1.6      val conjuncts =
     1.7 -      (Drule.equal_elim_rule2 OF [body_eq,
     1.8 -        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
     1.9 +      (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
    1.10        |> Conjunction.elim_balanced (length ts);
    1.11      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    1.12        Element.prove_witness defs_ctxt t