--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 24 11:07:50 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 24 13:55:02 2012 +0100
@@ -482,14 +482,6 @@
| _ => false
end
-(*Given a list of "'a option", apply an ('a -> 'b) function to each
-element s.t. the function is only applied if that element isn't NONE*)
-fun map_opt f xs =
- map (fn x =>
- if is_some x then
- SOME (f (the x))
- else NONE) xs
-
(*
Information needed to be carried around:
- constant mapping: maps constant names to Isabelle terms with fully-qualified
@@ -625,7 +617,7 @@
let
val var_types' =
ListPair.unzip bindings
- |> (apsnd (map_opt (interpret_type config thy type_map)))
+ |> (apsnd ((map o Option.map) (interpret_type config thy type_map)))
|> ListPair.zip
|> List.rev
fun fold_bind f =