# HG changeset patch
# User huffman
# Date 1291132850 28800
# Node ID 86dff9dfd8069b84dcaf7f974dd4cb06126d1672
# Parent  63276d22ea6028649c7975dfb2ced64f3c2cef89# Parent  eeaa59fb5ad82346bdb9e9f88223b52e40080920
merged

diff -r 63276d22ea60 -r 86dff9dfd806 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Nov 29 14:37:40 2010 -0800
+++ b/src/HOL/SMT.thy	Tue Nov 30 08:00:50 2010 -0800
@@ -324,6 +324,7 @@
   "(if P then True else False) = P"
   "(if P then False else True) = (\<not>P)"
   "(if \<not>P then x else y) = (if P then y else x)"
+  "f (if P then x else y) = (if P then f x else f y)"
   by auto
 
 lemma [z3_rule]:
diff -r 63276d22ea60 -r 86dff9dfd806 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 29 14:37:40 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Nov 30 08:00:50 2010 -0800
@@ -73,8 +73,13 @@
   |> Option.map (fn inst => Thm.instantiate inst thm)
 
 fun net_instance' f net ct =
-  let fun first_of f xthms ct = get_first (f (maybe_instantiate ct)) xthms 
-  in first_of f (Net.match_term net (Thm.term_of ct)) ct end
+  let
+    val xthms = Net.match_term net (Thm.term_of ct)
+    fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
+    fun first_of' f ct =
+      let val thm = Thm.trivial ct
+      in get_first (f (try (fn rule => rule COMP thm))) xthms end
+  in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
 val net_instance = net_instance' I