# HG changeset patch
# User wenzelm
# Date 1116773472 -7200
# Node ID ffe25459c72a3fb80a51bc998dac546faa3ecefa
# Parent  66561f6814bdb9ddafc38e08e1aa8ef75b32d162
tuned terms_of_tpairs;

diff -r 66561f6814bd -r ffe25459c72a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun May 22 16:51:11 2005 +0200
+++ b/src/Pure/thm.ML	Sun May 22 16:51:12 2005 +0200
@@ -300,7 +300,7 @@
   tpairs: (term * term) list,  (*flex-flex pairs*)
   prop: term};                 (*conclusion*)
 
-fun terms_of_tpairs tpairs = List.concat (map (op @ o pairself single) tpairs);
+fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs);
 
 fun attach_tpairs tpairs prop =
   Logic.list_implies (map Logic.mk_equals tpairs, prop);