tuned terms_of_tpairs;

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