--- a/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:12 2014 +0200
@@ -41,7 +41,7 @@
val ss = the_list (AList.lookup (op =) fact_helper_ids id)
val name0 = (sid ^ "a", ss)
val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids
- fact_helper_ts hyp_ts concl_t concl
+ fact_helper_ts hyp_ts concl_t concl ||> unskolemize_names
in
[(name0, role0, concl0, rule, []),
((sid, []), Plain, concl', veriT_rewrite_rule,