# HG changeset patch # User blanchet # Date 1402506512 -7200 # Node ID 7e90e30822a9b55776b48dd4e611d7220996dc5a # Parent 159c18bbc879e74df7c529564693b944b7f74224 simplify slightly ATP proof generated for Z3 diff -r 159c18bbc879 -r 7e90e30822a9 src/HOL/Tools/SMT2/z3_new_isar.ML --- 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]