dropped infix union
authorhaftmann
Fri Mar 27 12:22:02 2009 +0100 (2009-03-27)
changeset 307432c83f7eaf1a4
parent 30742 3e89ac3905b9
child 30744 50ccaef52871
dropped infix union
src/HOL/Library/reflection.ML
     1.1 --- a/src/HOL/Library/reflection.ML	Fri Mar 27 12:22:01 2009 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Mar 27 12:22:02 2009 +0100
     1.3 @@ -243,8 +243,8 @@
     1.4  		     insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop 
     1.5  			 |> HOLogic.dest_eq |> fst |> strip_comb 
     1.6  			 |> fst)) raw_eqs []
     1.7 -  val tys = fold_rev (fn f => fn ts => (f |> fastype_of |> binder_types |> tl) 
     1.8 -				    union ts) fs []
     1.9 +  val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl) 
    1.10 +				    ) fs []
    1.11    val _ = bds := AList.make (fn _ => ([],[])) tys
    1.12    val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
    1.13    val thy = ProofContext.theory_of ctxt'