--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jun 11 16:02:10 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jun 11 19:08:32 2014 +0200
@@ -130,8 +130,9 @@
else
NONE)
in
- [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
- ((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
+ (if role0 = Axiom then []
+ else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
+ [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
name0 :: normalize_prems)]
end
| Z3_New_Proof.Rewrite => [standard_step Lemma]