# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 31f5781fa9cd58dcaa6506f021cc519dc98efb23
# Parent  816f96fff418c9758b7473839f3ce52e176801cc
tuned order of arguments

diff -r 816f96fff418 -r 31f5781fa9cd src/HOL/Tools/SMT2/smtlib2_isar.ML
--- 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 @
diff -r 816f96fff418 -r 31f5781fa9cd src/HOL/Tools/SMT2/smtlib2_proof.ML
--- 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
 
diff -r 816f96fff418 -r 31f5781fa9cd src/HOL/Tools/SMT2/verit_isar.ML
--- 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
diff -r 816f96fff418 -r 31f5781fa9cd src/HOL/Tools/SMT2/z3_new_isar.ML
--- 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)