src/HOL/Tools/SMT/z3_isar.ML
changeset 60924 610794dff23c
parent 59013 f319054e8dff
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Tools/SMT/z3_isar.ML	Wed Aug 12 21:38:39 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_isar.ML	Thu Aug 13 11:05:19 2015 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  
     1.5  val reorder_foralls =
     1.6    dest_alls
     1.7 -  #>> sort_wrt fst
     1.8 +  #>> sort_by fst
     1.9    #-> fold_rev (Logic.all o Free);
    1.10  
    1.11  fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids