--- 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 =
--- 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