--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jul 30 14:03:12 2014 +0200
@@ -87,12 +87,11 @@
distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
hyp_ts concl_t concl
- val normalizing_prems = normalize_prems ctxt concl0
in
(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 :: normalizing_prems)]
+ name0 :: normalizing_prems ctxt concl0)]
end
| Z3_New_Proof.Rewrite => [standard_step Lemma]
| Z3_New_Proof.Rewrite_Star => [standard_step Lemma]