--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -65,7 +65,6 @@
|> not (null ll_defs) ? unlift_term ll_defs
|> unskolemize_names
|> HOLogic.mk_Trueprop
- |> unskolemize_names
fun normalizing_prems ctxt concl0 =
SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
--- a/src/HOL/Tools/SMT2/verit_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -42,7 +42,7 @@
val name0 = (id ^ "a", ss)
val concl0 = unskolemize_names concl00
in
- [(name0, role0, unskolemize_names concl0, rule, []),
+ [(name0, role0, concl0, rule, []),
((id, []), Plain, concl', veriT_rewrite_rule,
name0 :: normalizing_prems ctxt concl0)]
end)
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Aug 01 14:43:57 2014 +0200
@@ -83,8 +83,11 @@
(case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
hyp_ts concl_t concl of
NONE => []
- | SOME (role0, concl0) =>
- let val name0 = (sid ^ "a", ss) in
+ | SOME (role0, concl00) =>
+ let
+ val name0 = (sid ^ "a", ss)
+ val concl0 = unskolemize_names concl00
+ 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,