use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Apr 08 19:04:08 2011 +0200
@@ -63,15 +63,23 @@
   try Thm.first_order_match (Thm.cprop_of thm, ct)
   |> Option.map (fn inst => Thm.instantiate inst thm)
 
-fun net_instance' f net ct =
-  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
+local
+  fun instances_from_net match f net ct =
+    let
+      val lookup = if match then Net.match_term else Net.unify_term
+      val xthms = lookup 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
+in
+
+fun net_instance' f = instances_from_net false f
+
+val net_instance = instances_from_net true I
+
+end