subtract (op =);

--- a/src/Pure/IsaPlanner/isand.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/IsaPlanner/isand.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -223,7 +223,7 @@
 fun unfix_tfrees ns th = 
     let 
       val varfiytfrees = (map (fn x => Term.dest_TFree (Thm.typ_of x)) ns)
-      val skiptfrees = Term.add_term_tfrees (Thm.prop_of th,[]) \\ varfiytfrees;
+      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
     in #2 (Thm.varifyT' skiptfrees th) end;
 
 (* change schematic/meta vars to fresh free vars *)

--- a/src/Pure/Isar/obtain.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -208,7 +208,7 @@
     val rule' = rule |> Thm.instantiate (instT, []);
 
     val tvars = Drule.tvars_of rule';
-    val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
+    val vars = subtract (op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
     val _ =
       if null tvars andalso null vars then ()
       else err ("Illegal schematic variable(s) " ^

--- a/src/Pure/Syntax/syntax.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -243,7 +243,7 @@
     val {input, lexicon, gram, consts, prmodes,
       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
       print_ast_trtab, tokentrtab, prtabs} = tabs;
-    val input' = if inout then fold (remove (op =)) xprods input else input;
+    val input' = if inout then subtract (op =) xprods input else input;
   in
     Syntax
     ({input = input',

--- a/src/Pure/Tools/class_package.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -521,11 +521,11 @@
             andalso Sign.typ_instance thy (ty1', ty2')
             andalso Sign.typ_instance thy (ty2', ty1')
           end;
-        val _ = case fold (remove eq_c) c_req c_given
+        val _ = case subtract eq_c c_req c_given
          of [] => ()
           | cs => error ("superfluous definition(s) given for "
                     ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
-        val _ = case fold (remove eq_c) c_given c_req
+        val _ = case subtract eq_c c_given c_req
          of [] => ()
           | cs => error ("no definition(s) given for "
                     ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);

--- a/src/Pure/Tools/codegen_thingol.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -514,8 +514,8 @@
         val preds_ = Graph.imm_preds modl key;
         val succs_ = Graph.imm_succs modl key;
         val mutbs = gen_inter (op =) (preds_, succs_);
-        val preds = fold (remove (op =)) mutbs preds_;
-        val succs = fold (remove (op =)) mutbs succs_;
+        val preds = subtract (op =) mutbs preds_;
+        val succs = subtract (op =) mutbs succs_;
       in
         (Pretty.block o Pretty.fbreaks) (
           Pretty.str key
@@ -1116,4 +1116,4 @@
 
 end; (* struct *)
 
-structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;
\ No newline at end of file
+structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;

--- a/src/Pure/display.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/display.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -76,7 +76,7 @@
     val q = if quote then Pretty.quote else I;
     val prt_term = q o (Pretty.term pp);
 
-    val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
+    val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
     val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
     val hlen = length xshyps + length hyps' + length tpairs;
     val hsymbs =

--- a/src/Pure/pattern.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/pattern.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -74,7 +74,7 @@
   then let val f = Syntax.string_of_vname F
            val xs = bnames binders is
            val u = string_of_term thy env binders t
-           val ys = bnames binders (loose_bnos t \\ is)
+           val ys = bnames binders (subtract (op =) is (loose_bnos t))
        in tracing("Cannot unify variable " ^ f ^
                " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
                "\nTerm contains additional bound variable(s) " ^ ys)

--- a/src/Pure/proof_general.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/proof_general.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -1428,7 +1428,7 @@
   change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   init_pgip_session_id ();
   if pgip then
-    change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN])
+    change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN])
   else
     pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
   set_prompts isar pgip;