# HG changeset patch
# User boehmes
# Date 1291072349 -3600
# Node ID eeaa59fb5ad82346bdb9e9f88223b52e40080920
# Parent  59d96f777da3554cd5e8135968335ec3dbf05a33# Parent  5a195f11ef46b17c4d9b3ad8993c66e2b82898ca
merged

diff -r 5a195f11ef46 -r eeaa59fb5ad8 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Nov 29 16:10:44 2010 +0100
+++ b/src/HOL/SMT.thy	Tue Nov 30 00:12:29 2010 +0100
@@ -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 5a195f11ef46 -r eeaa59fb5ad8 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 29 16:10:44 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Nov 30 00:12:29 2010 +0100
@@ -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