--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Jun 12 01:00:49 2014 +0200
@@ -43,7 +43,7 @@
let
val lookup = if match then Net.match_term else Net.unify_term
val xthms = lookup net (Thm.term_of ct)
- fun select ct = map_filter (f (maybe_instantiate ct)) xthms
+ fun select ct = map_filter (f (maybe_instantiate ct)) xthms
fun select' ct =
let val thm = Thm.trivial ct
in map_filter (f (try (fn rule => rule COMP thm))) xthms end