modernized some old-style infix operations, which were left over from the time of ML proof scripts;

--- a/NEWS	Thu Nov 24 20:45:34 2011 +0100
+++ b/NEWS	Thu Nov 24 21:01:06 2011 +0100
@@ -173,6 +173,12 @@
   deleqcongs    ~> Simplifier.del_eqcong
   addcongs      ~> Simplifier.add_cong
   delcongs      ~> Simplifier.del_cong
+  setmksimps    ~> Simplifier.set_mksimps
+  setmkcong     ~> Simplifier.set_mkcong
+  setmksym      ~> Simplifier.set_mksym
+  setmkeqTrue   ~> Simplifier.set_mkeqTrue
+  settermless   ~> Simplifier.set_termless
+  setsubgoaler  ~> Simplifier.set_subgoaler
   addsplits     ~> Splitter.add_split
   delsplits     ~> Splitter.del_split
 

--- a/src/FOL/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/FOL/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -116,11 +116,11 @@
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
   Simplifier.global_context @{theory} empty_ss
-  setsubgoaler asm_simp_tac
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)
-  setmksimps (mksimps mksimps_pairs)
-  setmkcong mk_meta_cong;
+  |> Simplifier.set_subgoaler asm_simp_tac
+  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
+  |> Simplifier.set_mkcong mk_meta_cong;
 
 fun unfold_tac ths =
   let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths

--- a/src/HOL/Algebra/abstract/Ring2.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -210,7 +210,9 @@
 
 fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
 
-val ring_ss = HOL_basic_ss settermless termless_ring addsimps
+val ring_ss =
+  (HOL_basic_ss |> Simplifier.set_termless termless_ring)
+  addsimps
   [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
    @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
    @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},

--- a/src/HOL/Algebra/ringsimp.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -47,7 +47,7 @@
     fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
       | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
     fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
-  in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
+  in asm_full_simp_tac (HOL_ss addsimps simps |> Simplifier.set_termless less) end;
 
 fun algebra_tac ctxt =
   EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));

--- a/src/HOL/HOL.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/HOL.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -1495,9 +1495,6 @@
 setup {*
   Induct.setup #> Induction.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
-    setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
-      map (Simplifier.rewrite_rule (map Thm.symmetric
-        @{thms induct_rulify_fallback})))
     addsimprocs
       [Simplifier.simproc_global @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]
@@ -1517,7 +1514,10 @@
                     | is_conj @{const induct_false} = true
                     | is_conj _ = false
                 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
-              | _ => NONE))]))
+              | _ => NONE))]
+    |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
+      map (Simplifier.rewrite_rule (map Thm.symmetric
+        @{thms induct_rulify_fallback})))))
 *}
 
 text {* Pre-simplification of induction and cases rules *}

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -67,7 +67,7 @@
   "Finite (mksch A B$tr$x$y) --> Finite tr"
 
 
-declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (K NONE))) *}
+declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
 
 
 subsection "mksch rewrite rules"
@@ -967,7 +967,7 @@
 done
 
 
-declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K (SOME o symmetric_fun))) *}
+declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (SOME o symmetric_fun))) *}
 
 
 end

--- a/src/HOL/Nominal/Nominal.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -378,7 +378,7 @@
   val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
 *}
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
 *}
 
 section {* Abstract Properties for Permutations and  Atoms *}

--- a/src/HOL/Prolog/prolog.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Prolog/prolog.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -59,14 +59,15 @@
 in map zero_var_indexes (at thm) end;
 
 val atomize_ss =
-  Simplifier.global_context @{theory} empty_ss
-  setmksimps (mksimps mksimps_pairs)
+  (Simplifier.global_context @{theory} empty_ss
+    |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   addsimps [
         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
         imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
+
 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
                                   resolve_tac (maps atomizeD prems) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)

--- a/src/HOL/Set.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Set.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -369,7 +369,7 @@
 *}
 
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
 *}
 
 lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -31,8 +31,8 @@
 (* need to set up our own minimal simpset.    *)
 fun mk_minimal_ss ctxt =
   Simplifier.context ctxt empty_ss
-    setsubgoaler asm_simp_tac
-    setmksimps (mksimps [])
+  |> Simplifier.set_subgoaler asm_simp_tac
+  |> Simplifier.set_mksimps (mksimps [])
 
 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1

--- a/src/HOL/Tools/abel_cancel.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/abel_cancel.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -91,7 +91,7 @@
 val simproc = Simplifier.simproc_global @{theory}
   "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
 
-val cancel_ss = HOL_basic_ss settermless less_agrp
+val cancel_ss = (HOL_basic_ss |> Simplifier.set_termless less_agrp)
   addsimprocs [simproc] addsimps
   [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
    @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},

--- a/src/HOL/Tools/lin_arith.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -704,8 +704,9 @@
 
 local
   val nnf_simpset =
-    empty_ss setmkeqTrue mk_eq_True
-    setmksimps (mksimps mksimps_pairs)
+    (empty_ss
+      |> Simplifier.set_mkeqTrue mk_eq_True
+      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
       @{thm de_Morgan_conj}, not_all, not_ex, not_not]
   fun prem_nnf_tac ss = full_simp_tac (Simplifier.inherit_context ss nnf_simpset)
@@ -838,8 +839,9 @@
 
 local
   val nnf_simpset =
-    empty_ss setmkeqTrue mk_eq_True
-    setmksimps (mksimps mksimps_pairs)
+    (empty_ss
+      |> Simplifier.set_mkeqTrue mk_eq_True
+      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
       @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
   fun prem_nnf_tac i st =

--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -169,7 +169,7 @@
 
 fun numtermless tu = (numterm_ord tu = LESS);
 
-val num_ss = HOL_ss settermless numtermless;
+val num_ss = HOL_ss |> Simplifier.set_termless numtermless;
 
 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];

--- a/src/HOL/Tools/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/HOL/Tools/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -167,12 +167,12 @@
 
 val HOL_basic_ss =
   Simplifier.global_context @{theory} empty_ss
-    setsubgoaler asm_simp_tac
-    setSSolver safe_solver
-    setSolver unsafe_solver
-    setmksimps (mksimps mksimps_pairs)
-    setmkeqTrue mk_eq_True
-    setmkcong mk_meta_cong;
+  setSSolver safe_solver
+  setSolver unsafe_solver
+  |> Simplifier.set_subgoaler asm_simp_tac
+  |> Simplifier.set_mksimps (mksimps mksimps_pairs)
+  |> Simplifier.set_mkeqTrue mk_eq_True
+  |> Simplifier.set_mkcong mk_meta_cong;
 
 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
 

--- a/src/Provers/hypsubst.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/Provers/hypsubst.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -131,7 +131,7 @@
       let
         val (k, _) = eq_var bnd true Bi
         val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
-          setmksimps (K (mk_eqs bnd))
+          |> Simplifier.set_mksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st

--- a/src/Pure/raw_simplifier.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -6,8 +6,8 @@
 
 infix 4
   addsimps delsimps addsimprocs delsimprocs
-  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
-  setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
+  setloop' setloop addloop addloop' delloop
+  setSSolver addSSolver setSolver addSolver;
 
 signature BASIC_RAW_SIMPLIFIER =
 sig
@@ -41,13 +41,6 @@
   val delsimps: simpset * thm list -> simpset
   val addsimprocs: simpset * simproc list -> simpset
   val delsimprocs: simpset * simproc list -> simpset
-  val mksimps: simpset -> thm -> thm list
-  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
-  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
-  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
-  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
-  val settermless: simpset * (term * term -> bool) -> simpset
-  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   val setloop': simpset * (simpset -> int -> tactic) -> simpset
   val setloop: simpset * (int -> tactic) -> simpset
   val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
@@ -99,6 +92,13 @@
   val del_eqcong: thm -> simpset -> simpset
   val add_cong: thm -> simpset -> simpset
   val del_cong: thm -> simpset -> simpset
+  val mksimps: simpset -> thm -> thm list
+  val set_mksimps: (simpset -> thm -> thm list) -> simpset -> simpset
+  val set_mkcong: (simpset -> thm -> thm) -> simpset -> simpset
+  val set_mksym: (simpset -> thm -> thm option) -> simpset -> simpset
+  val set_mkeqTrue: (simpset -> thm -> thm option) -> simpset -> simpset
+  val set_termless: (term * term -> bool) -> simpset -> simpset
+  val set_subgoaler: (simpset -> int -> tactic) -> simpset -> simpset
   val solver: simpset -> solver -> int -> tactic
   val simp_depth_limit_raw: Config.raw
   val clear_ss: simpset -> simpset
@@ -685,16 +685,16 @@
 
 fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
 
-fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
+fun set_mksimps mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
-fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
+fun set_mkcong mk_cong = map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
-fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
+fun set_mksym mk_sym = map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
-fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
+fun set_mkeqTrue mk_eq_True = map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
 
 fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
@@ -705,14 +705,14 @@
 
 (* termless *)
 
-fun ss settermless termless = ss |>
+fun set_termless termless =
   map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
 
 
 (* tactics *)
 
-fun ss setsubgoaler subgoal_tac = ss |>
+fun set_subgoaler subgoal_tac =
   map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
 

--- a/src/Pure/simplifier.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/Pure/simplifier.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -42,6 +42,13 @@
   val add_cong: thm -> simpset -> simpset
   val del_cong: thm -> simpset -> simpset
   val add_prems: thm list -> simpset -> simpset
+  val mksimps: simpset -> thm -> thm list
+  val set_mksimps: (simpset -> thm -> thm list) -> simpset -> simpset
+  val set_mkcong: (simpset -> thm -> thm) -> simpset -> simpset
+  val set_mksym: (simpset -> thm -> thm option) -> simpset -> simpset
+  val set_mkeqTrue: (simpset -> thm -> thm option) -> simpset -> simpset
+  val set_termless: (term * term -> bool) -> simpset -> simpset
+  val set_subgoaler: (simpset -> int -> tactic) -> simpset -> simpset
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
@@ -415,10 +422,11 @@
 
     fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
   in
-    empty_ss setsubgoaler asm_simp_tac
+    empty_ss
     setSSolver safe_solver
     setSolver unsafe_solver
-    setmksimps (K mksimps)
+    |> set_subgoaler asm_simp_tac
+    |> set_mksimps (K mksimps)
   end));
 
 end;

--- a/src/Sequents/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/Sequents/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -68,11 +68,11 @@
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
   Simplifier.global_context @{theory} empty_ss
-    setsubgoaler asm_simp_tac
-    setSSolver (mk_solver "safe" safe_solver)
-    setSolver (mk_solver "unsafe" unsafe_solver)
-    setmksimps (K (map mk_meta_eq o atomize o gen_all))
-    setmkcong mk_meta_cong;
+  setSSolver (mk_solver "safe" safe_solver)
+  setSolver (mk_solver "unsafe" unsafe_solver)
+  |> Simplifier.set_subgoaler asm_simp_tac
+  |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all))
+  |> Simplifier.set_mkcong mk_meta_cong;
 
 val LK_simps =
    [triv_forall_equality, (* prunes params *)

--- a/src/ZF/Main_ZF.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/ZF/Main_ZF.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -71,7 +71,7 @@
 
 
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
+  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
 *}
 
 end

--- a/src/ZF/OrdQuant.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/ZF/OrdQuant.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -363,7 +363,7 @@
              ZF_mem_pairs);
 *}
 declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all)))
+  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
 *}
 
 text {* Setting up the one-point-rule simproc *}

--- a/src/ZF/Tools/inductive_package.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -326,8 +326,9 @@
 
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
-     val min_ss = Simplifier.global_context thy empty_ss
-           setmksimps (K (map mk_eq o ZF_atomize o gen_all))
+     val min_ss =
+           (Simplifier.global_context thy empty_ss
+             |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
            setSolver (mk_solver "minimal"
                       (fn ss => resolve_tac (triv_rls @ Simplifier.prems_of ss)
                                    ORELSE' assume_tac

--- a/src/ZF/pair.thy	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/ZF/pair.thy	Thu Nov 24 21:01:06 2011 +0100
@@ -10,9 +10,9 @@
 begin
 
 setup {*
-  Simplifier.map_simpset_global (fn ss =>
-    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
-    |> Simplifier.add_cong @{thm if_weak_cong})
+  Simplifier.map_simpset_global
+    (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
+      #> Simplifier.add_cong @{thm if_weak_cong})
 *}
 
 ML {* val ZF_ss = @{simpset} *}