src/Pure/term_items.ML

   Table (if Table.defined tab x then tab else Table.update_new (x, Table.size tab + 1) tab);
 
 fun make_set xs = build (fold add_set xs);
 
 fun subset (A: set, B: set) = forall (defined B o #1) A;
-fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+fun eq_set (A: set, B: set) = pointer_eq (A, B) orelse size A = size B andalso subset (A, B);
 
 fun list_set_ord ord (Table tab) = tab |> Table.dest |> sort (ord o apply2 #2) |> map #1;
 val list_set = list_set_ord int_ord;
 val list_set_rev = list_set_ord (rev_order o int_ord);