1.1 --- a/src/Provers/induct_method.ML	Sat Jul 28 20:40:26 2007 +0200
     1.2 +++ b/src/Provers/induct_method.ML	Sat Jul 28 20:40:27 2007 +0200
     1.3 @@ -476,10 +476,10 @@
     1.4    | single_rule _ = error "Single rule expected";
     1.5  
     1.6  fun named_rule k arg get =
     1.7 -  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :--
     1.8 +  Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
     1.9      (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
    1.10        (case get (Context.proof_of context) name of SOME x => x
    1.11 -      | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2;
    1.12 +      | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
    1.13  
    1.14  fun rule get_type get_set =
    1.15    named_rule InductAttrib.typeN Args.tyname get_type ||

     2.1 --- a/src/Pure/Isar/attrib.ML	Sat Jul 28 20:40:26 2007 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sat Jul 28 20:40:27 2007 +0200
     2.3 @@ -204,14 +204,14 @@
     2.4    | scan_value (ConfigOption.String _) = (equals |-- Args.name) >> ConfigOption.String;
     2.5  
     2.6  fun scan_config x =
     2.7 -  ((Args.name >> ConfigOption.the_option) :-- (fn (config, config_type) =>
     2.8 +  ((Args.name >> ConfigOption.the_option) :|-- (fn (config, config_type) =>
     2.9      scan_value config_type >> (fn value =>
    2.10 -      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value))))) >> #2) x;
    2.11 +      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value)))))) x;
    2.12  
    2.13  fun scan_att x =
    2.14    (Args.internal_attribute ||
    2.15 -    (Scan.ahead (scan_config --| Args.terminator) :--
    2.16 -      (fn att => Args.named_attribute (K att))) >> #2) x;
    2.17 +    (Scan.ahead (scan_config --| Args.terminator) :|--
    2.18 +      (fn att => Args.named_attribute (K att)))) x;
    2.19  
    2.20  in
    2.21  

     3.1 --- a/src/Pure/Isar/method.ML	Sat Jul 28 20:40:26 2007 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Sat Jul 28 20:40:27 2007 +0200
     3.3 @@ -468,8 +468,8 @@
     3.4  fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
     3.5  fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
     3.6  
     3.7 -fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :--
     3.8 -  (fn (m, ths) => Scan.succeed (app m (context, ths))) >> #2);
     3.9 +fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
    3.10 +  (fn (m, ths) => Scan.succeed (app m (context, ths))));
    3.11  
    3.12  fun sectioned args ss = args -- Scan.repeat (section ss);
    3.13  

     4.1 --- a/src/Pure/Isar/outer_lex.ML	Sat Jul 28 20:40:26 2007 +0200
     4.2 +++ b/src/Pure/Isar/outer_lex.ML	Sat Jul 28 20:40:27 2007 +0200
     4.3 @@ -300,7 +300,7 @@
     4.4  
     4.5  fun scan (lex1, lex2) =
     4.6    let
     4.7 -    val scanner = Scan.state :-- (fn pos =>
     4.8 +    val scanner = Scan.state :|-- (fn pos =>
     4.9        let
    4.10          fun token k x = Token (pos, (k, x));
    4.11          fun sync _ = token Sync Symbol.sync;
    4.12 @@ -323,7 +323,7 @@
    4.13              Syntax.scan_tvar >> token TypeVar ||
    4.14              Syntax.scan_nat >> token Nat ||
    4.15              scan_symid >> token SymIdent))
    4.16 -      end) >> #2;
    4.17 +      end);
    4.18    in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
    4.19  
    4.20  
    4.21 @@ -333,8 +333,8 @@
    4.22  
    4.23  val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular;
    4.24  
    4.25 -fun recover msg = Scan.state :-- (fn pos =>
    4.26 -  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))])) >> #2;
    4.27 +fun recover msg = Scan.state :|-- (fn pos =>
    4.28 +  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))]));
    4.29  
    4.30  in
    4.31  

     5.1 --- a/src/Pure/Tools/xml.ML	Sat Jul 28 20:40:26 2007 +0200
     5.2 +++ b/src/Pure/Tools/xml.ML	Sat Jul 28 20:40:27 2007 +0200
     5.3 @@ -132,8 +132,8 @@
     5.4  
     5.5  val parse_att =
     5.6    Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
     5.7 -  (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
     5.8 -    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
     5.9 +  (($$ "\"" || $$ "'") :|-- (fn s => (Scan.repeat (Scan.unless ($$ s)
    5.10 +    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s));
    5.11  
    5.12  val parse_comment = Scan.this_string "<!--" --
    5.13    Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --

     6.1 --- a/src/Pure/codegen.ML	Sat Jul 28 20:40:26 2007 +0200
     6.2 +++ b/src/Pure/codegen.ML	Sat Jul 28 20:40:27 2007 +0200
     6.3 @@ -1183,8 +1183,8 @@
     6.4     ("iterations", P.nat >> (K o set_iterations)),
     6.5     ("default_type", P.typ >> set_default_type)];
     6.6  
     6.7 -val parse_test_params = P.short_ident :-- (fn s =>
     6.8 -  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
     6.9 +val parse_test_params = P.short_ident :|-- (fn s =>
    6.10 +  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
    6.11  
    6.12  fun parse_tyinst xs =
    6.13    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>