# HG changeset patch
# User wenzelm
# Date 1185648027 -7200
# Node ID ab76c73b3b5845eedd953811b8c8006ac18c28f2
# Parent  491c68f40bc449d504c415eea181a3990e7fb896
tuned;

diff -r 491c68f40bc4 -r ab76c73b3b58 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Provers/induct_method.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -476,10 +476,10 @@
   | single_rule _ = error "Single rule expected";
 
 fun named_rule k arg get =
-  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
+  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
     (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
       (case get (Context.proof_of context) name of SOME x => x
-      | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
+      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
 
 fun rule get_type get_set =
   named_rule InductAttrib.typeN Args.tyname get_type ||
diff -r 491c68f40bc4 -r ab76c73b3b58 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -204,14 +204,14 @@
   | scan_value (ConfigOption.String _) = (equals |-- Args.name) >> ConfigOption.String;
 
 fun scan_config x =
-  ((Args.name >> ConfigOption.the_option) :-- (fn (config, config_type) =>
+  ((Args.name >> ConfigOption.the_option) :|-- (fn (config, config_type) =>
     scan_value config_type >> (fn value =>
-      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value))))) >> #2) x;
+      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value)))))) x;
 
 fun scan_att x =
   (Args.internal_attribute ||
-    (Scan.ahead (scan_config --| Args.terminator) :--
-      (fn att => Args.named_attribute (K att))) >> #2) x;
+    (Scan.ahead (scan_config --| Args.terminator) :|--
+      (fn att => Args.named_attribute (K att)))) x;
 
 in
 
diff -r 491c68f40bc4 -r ab76c73b3b58 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Pure/Isar/method.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -468,8 +468,8 @@
 fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
 fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
 
-fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :--
-  (fn (m, ths) => Scan.succeed (app m (context, ths))) >> #2);
+fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
+  (fn (m, ths) => Scan.succeed (app m (context, ths))));
 
 fun sectioned args ss = args -- Scan.repeat (section ss);
 
diff -r 491c68f40bc4 -r ab76c73b3b58 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -300,7 +300,7 @@
 
 fun scan (lex1, lex2) =
   let
-    val scanner = Scan.state :-- (fn pos =>
+    val scanner = Scan.state :|-- (fn pos =>
       let
         fun token k x = Token (pos, (k, x));
         fun sync _ = token Sync Symbol.sync;
@@ -323,7 +323,7 @@
             Syntax.scan_tvar >> token TypeVar ||
             Syntax.scan_nat >> token Nat ||
             scan_symid >> token SymIdent))
-      end) >> #2;
+      end);
   in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
 
 
@@ -333,8 +333,8 @@
 
 val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular;
 
-fun recover msg = Scan.state :-- (fn pos =>
-  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))])) >> #2;
+fun recover msg = Scan.state :|-- (fn pos =>
+  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))]));
 
 in
 
diff -r 491c68f40bc4 -r ab76c73b3b58 src/Pure/Tools/xml.ML
--- a/src/Pure/Tools/xml.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Pure/Tools/xml.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -132,8 +132,8 @@
 
 val parse_att =
   Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
-  (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
-    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
+  (($$ "\"" || $$ "'") :|-- (fn s => (Scan.repeat (Scan.unless ($$ s)
+    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s));
 
 val parse_comment = Scan.this_string "<!--" --
   Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
diff -r 491c68f40bc4 -r ab76c73b3b58 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Jul 28 20:40:26 2007 +0200
+++ b/src/Pure/codegen.ML	Sat Jul 28 20:40:27 2007 +0200
@@ -1183,8 +1183,8 @@
    ("iterations", P.nat >> (K o set_iterations)),
    ("default_type", P.typ >> set_default_type)];
 
-val parse_test_params = P.short_ident :-- (fn s =>
-  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
+val parse_test_params = P.short_ident :|-- (fn s =>
+  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
 
 fun parse_tyinst xs =
   (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>