introduced binding priority 1 for linear combinators etc.

--- a/src/HOL/Tools/record_package.ML	Sat Sep 03 22:27:06 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Sep 05 08:14:35 2005 +0200
@@ -1178,8 +1178,8 @@
    
     val simprocs = if has_rec goal then [record_split_simproc P] else [];
    
-  in st |> (EVERY split_frees_tacs) 
-           THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i)
+  in st |> ((EVERY split_frees_tacs) 
+           THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i))
   end handle Empty => Seq.empty;
 end;
 

--- a/src/Provers/blast.ML	Sat Sep 03 22:27:06 2005 +0200
+++ b/src/Provers/blast.ML	Mon Sep 05 08:14:35 2005 +0200
@@ -455,7 +455,7 @@
 
 
 (*Like dup_elim, but puts the duplicated major premise FIRST*)
-fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd;
 
 
 (*Rotate the assumptions in all new subgoals for the LIFO discipline*)

--- a/src/Provers/classical.ML	Sat Sep 03 22:27:06 2005 +0200
+++ b/src/Provers/classical.ML	Mon Sep 05 08:14:35 2005 +0200
@@ -212,7 +212,7 @@
 fun dup_elim th =
   (case try (fn () =>
     rule_by_tactic (TRYALL (etac revcut_rl))
-      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of
+      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd)) () of
     SOME th' => th'
   | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
 

--- a/src/Pure/Isar/locale.ML	Sat Sep 03 22:27:06 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 05 08:14:35 2005 +0200
@@ -1896,10 +1896,10 @@
       Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
 
     val conjuncts =
-      Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
-        Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
+      (Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
+        Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Drule.conj_elim_precise (length ts);
-    val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
+    val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Tactic.prove_plain defs_thy [] [] t (fn _ =>
         Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));

--- a/src/Pure/library.ML	Sat Sep 03 22:27:06 2005 +0200
+++ b/src/Pure/library.ML	Mon Sep 05 08:14:35 2005 +0200
@@ -8,14 +8,13 @@
 tables, balanced trees, orders, current directory, misc.
 *)
 
-infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
-  orf andf prefix upto downto mem mem_int mem_string union union_int
-  union_string inter inter_int inter_string subset subset_int
-  subset_string;
+infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
+infix 2 ?;
+infix 3 o oo ooo oooo;
 
-infix 2 ?;
-
-infix 3 oo ooo oooo;
+infix 4 ~~ upto downto;
+infix orf andf prefix \ \\ ins ins_string ins_int mem mem_int mem_string union union_int
+  union_string inter inter_int inter_string subset subset_int subset_string;
 
 signature BASIC_LIBRARY =
 sig