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