# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID ce40cee07fbc5909a7ec25fcdf5859874938a650
# Parent  31f5781fa9cd58dcaa6506f021cc519dc98efb23
reorder quantifiers to ease Z3 skolemization

diff -r 31f5781fa9cd -r ce40cee07fbc 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
@@ -63,6 +63,17 @@
           end
       end
 
+fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) =
+    let val (s', t') = Term.dest_abs abs in
+      dest_alls t' |>> cons (s', T)
+    end
+  | dest_alls t = ([], t)
+
+val reorder_foralls =
+  dest_alls
+  #>> sort_wrt fst
+  #-> fold_rev (Logic.all o Free);
+
 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
     conjecture_id fact_helper_ids proof =
   let
@@ -72,7 +83,9 @@
       let
         val sid = string_of_int id
 
-        val concl' = postprocess_step_conclusion thy rewrite_rules ll_defs concl
+        val concl' = concl
+          |> reorder_foralls (* crucial for skolemization steps *)
+          |> postprocess_step_conclusion thy rewrite_rules ll_defs
         fun standard_step role =
           ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
            map (fn id => (string_of_int id, [])) prems)