--- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Wed Nov 26 20:05:34 2014 +0100
@@ -262,7 +262,7 @@
| NONE =>
(case lookup_rule t of
(rewrite, SOME lit) => (s, rewrite lit)
- | (_, NONE) => (s, comp (pairself join1 (dest t)))))
+ | (_, NONE) => (s, comp (apply2 join1 (dest t)))))
in snd (join1 (if is_conj then (false, t) else (true, t))) end
@@ -299,7 +299,7 @@
SOME rs => extract_lit thm rs
| NONE =>
the (Termtab.get_first contra_lits rules)
- |> pairself (extract_lit thm)
+ |> apply2 (extract_lit thm)
|> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
end