Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped infix union
authorhaftmann
Fri, 27 Mar 2009 12:22:02 +0100
changeset 30743 2c83f7eaf1a4
parent 30742 3e89ac3905b9
child 30744 50ccaef52871
dropped infix union
src/HOL/Library/reflection.ML file | annotate | diff | comparison | revisions 
--- 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'
isabelle