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