# HG changeset patch
# User blanchet
# Date 1394713093 -3600
# Node ID fb160b829a8855e79eb2c7ee1ee19eb3997513f3
# Parent  3d11892ea537e42c33d7c19ac79fa5a7eac53553
repaired 'if' logic

diff -r 3d11892ea537 -r fb160b829a88 src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -278,7 +278,7 @@
 
     val xthms = map (apsnd snd) xwthms
 
-    val filter_thms = if supports_filter ctxt then K xthms else map_filter (try (nth xthms))
+    val filter_thms = if supports_filter ctxt then map_filter (try (nth xthms)) else K xthms
   in
     map snd xwthms
     |> map_index I