--- 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]:
--- 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