remove (op =);
authorwenzelm
Tue Mar 21 12:18:06 2006 +0100 (2006-03-21)
changeset 192995f0610aafc48
parent 19298 741b8138c2b3
child 19300 7689f81f8996
remove (op =);
src/Provers/ind.ML
src/Pure/codegen.ML
     1.1 --- a/src/Provers/ind.ML	Tue Mar 21 12:17:38 2006 +0100
     1.2 +++ b/src/Provers/ind.ML	Tue Mar 21 12:18:06 2006 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  fun all_frees_tac (var:string) i thm = 
     1.5      let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
     1.6          val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
     1.7 -        val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
     1.8 +        val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
     1.9      in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
    1.10  
    1.11  fun REPEAT_SIMP_TAC simp_tac n i =
     2.1 --- a/src/Pure/codegen.ML	Tue Mar 21 12:17:38 2006 +0100
     2.2 +++ b/src/Pure/codegen.ML	Tue Mar 21 12:18:06 2006 +0100
     2.3 @@ -1137,8 +1137,7 @@
     2.4     || Scan.repeat1 (P.term >> pair "")) >>
     2.5    (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
     2.6       let
     2.7 -       val mode'' = if lib then "library" ins (mode' \ "library")
     2.8 -         else mode' \ "library";
     2.9 +       val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
    2.10         val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
    2.11       in ((case opt_fname of
    2.12           NONE => use_text Context.ml_output false