src/Tools/IsaPlanner/rw_inst.ML
changeset 33037 b22e44496dc2
parent 30190 479806475f3c
child 33038 8f9594c31de4
     1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -139,13 +139,13 @@
     1.4        val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
     1.5        val (conds_tyvs,cond_vs) = 
     1.6            Library.foldl (fn ((tyvs, vs), t) => 
     1.7 -                    (Library.union
     1.8 +                    (gen_union (op =)
     1.9                         (OldTerm.term_tvars t, tyvs),
    1.10 -                     Library.union 
    1.11 +                     gen_union (op =)
    1.12                         (map Term.dest_Var (OldTerm.term_vars t), vs))) 
    1.13                  (([],[]), rule_conds);
    1.14        val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
    1.15 -      val vars_to_fix = Library.union (termvars, cond_vs);
    1.16 +      val vars_to_fix = gen_union (op =) (termvars, cond_vs);
    1.17        val (renamings, names2) = 
    1.18            List.foldr (fn (((n,i),ty), (vs, names')) => 
    1.19                      let val n' = Name.variant names' n in