--- a/src/Pure/Isar/expression.ML Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/Isar/expression.ML Thu May 30 12:35:40 2013 +0200
@@ -671,8 +671,7 @@
Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
val conjuncts =
- (Drule.equal_elim_rule2 OF [body_eq,
- Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
+ (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