# HG changeset patch
# User wenzelm
# Date 1142939886 -3600
# Node ID 5f0610aafc4874c3eeb51727c53ad0af4a75ab04
# Parent  741b8138c2b35394ebd649179ab194e92144700a
remove (op =);

diff -r 741b8138c2b3 -r 5f0610aafc48 src/Provers/ind.ML
--- a/src/Provers/ind.ML	Tue Mar 21 12:17:38 2006 +0100
+++ b/src/Provers/ind.ML	Tue Mar 21 12:18:06 2006 +0100
@@ -42,7 +42,7 @@
 fun all_frees_tac (var:string) i thm = 
     let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
         val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
-        val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
+        val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
     in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
 
 fun REPEAT_SIMP_TAC simp_tac n i =
diff -r 741b8138c2b3 -r 5f0610aafc48 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Mar 21 12:17:38 2006 +0100
+++ b/src/Pure/codegen.ML	Tue Mar 21 12:18:06 2006 +0100
@@ -1137,8 +1137,7 @@
    || Scan.repeat1 (P.term >> pair "")) >>
   (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
      let
-       val mode'' = if lib then "library" ins (mode' \ "library")
-         else mode' \ "library";
+       val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
          NONE => use_text Context.ml_output false