--- 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
@@ -9,7 +9,7 @@
sig
val simplify_bool: term -> term
val unlift_term: term list -> term -> term
- val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term
+ val postprocess_step_conclusion: theory -> thm list -> term list -> term -> term
val normalizing_prems : Proof.context -> term -> (string * string list) list
val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
(''a * 'c) list -> 'c list -> 'c -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
@@ -57,14 +57,13 @@
Term.map_abs_vars (perhaps (try Name.dest_skolem))
#> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
-fun postprocess_step_conclusion concl thy rewrite_rules ll_defs =
- concl
- |> Raw_Simplifier.rewrite_term thy rewrite_rules []
- |> Object_Logic.atomize_term thy
- |> simplify_bool
- |> not (null ll_defs) ? unlift_term ll_defs
- |> unskolemize_names
- |> HOLogic.mk_Trueprop
+fun postprocess_step_conclusion thy rewrite_rules ll_defs =
+ Raw_Simplifier.rewrite_term thy rewrite_rules []
+ #> Object_Logic.atomize_term thy
+ #> simplify_bool
+ #> not (null ll_defs) ? unlift_term ll_defs
+ #> unskolemize_names
+ #> HOLogic.mk_Trueprop
fun normalizing_prems ctxt concl0 =
SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
--- a/src/HOL/Tools/SMT2/smtlib2_proof.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_proof.ML Fri Aug 01 14:43:57 2014 +0200
@@ -81,7 +81,7 @@
fun next_id ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) =
(id, mk_context ctxt (id + 1) syms typs funs extra)
-fun with_fresh_names f ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) =
+fun with_fresh_names f ({ctxt, id, syms, typs, funs, ...}: ('a, 'b) context) =
let
fun bind (_, v as (_, T)) t = Logic.all_const T $ Term.absfree v t
--- 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
@@ -29,7 +29,7 @@
val thy = Proof_Context.theory_of ctxt
fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
let
- val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
+ val concl' = postprocess_step_conclusion thy rewrite_rules ll_defs concl
fun standard_step role = ((id, []), role, concl', rule, map (fn id => (id, [])) prems)
in
if rule = veriT_input_rule then
--- 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
@@ -72,7 +72,7 @@
let
val sid = string_of_int id
- val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
+ val concl' = postprocess_step_conclusion thy rewrite_rules ll_defs concl
fun standard_step role =
((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
map (fn id => (string_of_int id, [])) prems)