# HG changeset patch
# User sultana
# Date 1335272102 -3600
# Node ID 44d1f4e0a46e7a18961ba3c8affc38561d079c6e
# Parent  b11dac707c789c018639759ab32ad2612c45ea7e
tuned;

diff -r b11dac707c78 -r 44d1f4e0a46e src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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 =