# HG changeset patch
# User haftmann
# Date 1238152922 -3600
# Node ID 2c83f7eaf1a4f1122c2b27a14953db6cee0f1806
# Parent  3e89ac3905b9b837249670d0a73985a087af34f1
dropped infix union

diff -r 3e89ac3905b9 -r 2c83f7eaf1a4 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Fri Mar 27 12:22:01 2009 +0100
+++ b/src/HOL/Library/reflection.ML	Fri Mar 27 12:22:02 2009 +0100
@@ -243,8 +243,8 @@
 		     insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop 
 			 |> HOLogic.dest_eq |> fst |> strip_comb 
 			 |> fst)) raw_eqs []
-  val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl) 
-				    union ts) fs []
+  val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl) 
+				    ) fs []
   val _ = bds := AList.make (fn _ => ([],[])) tys
   val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
   val thy = ProofContext.theory_of ctxt'