src/Pure/Proof/reconstruct.ML
changeset 19305 5c16895d548b
parent 18929 d81435108688
child 19419 2d26166aca27
--- a/src/Pure/Proof/reconstruct.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -246,7 +246,7 @@
       (Vartab.foldl (add_term_ixns o apsnd (snd o snd)) ([], asol), iTs);
     fun check_cs [] = []
       | check_cs ((u, p, vs)::ps) =
-          let val vs' = vs \\ dom;
+          let val vs' = subtract (op =) dom vs;
           in if vs = vs' then (u, p, vs)::check_cs ps
              else (true, p, vs' union vran)::check_cs ps
           end