Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_satallax.ML
changeset 57716 4546c9fdd8a7
parent 57714 4856a7b8b9c3
child 58043 a90847f03ec8 
--- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:58 2014 +0200
@@ -30,7 +30,7 @@
   ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id))
   -- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",")
   -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id
-         -- Scan.repeat ($$ "," |-- scan_general_id)) >> (op ::)) --| $$ "]"))
+         -- Scan.repeat ($$ "," |-- scan_general_id)) >> op ::) --| $$ "]"))
          || (skip_term >> K "") >> (fn x => SOME [x]))
        >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
 
@@ -39,12 +39,12 @@
 
 fun parse_prems x =
   (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]")
-     >> (op ::)) x
+     >> op ::) x
 
 fun parse_tstp_satallax_extra_arguments x =
   ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," )
   -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information
-  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> (op ::))
+  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> op ::)
   --| $$ "]") --
   (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) []
     >> (fn (x, []) => x | (_, x) => x))
isabelle