src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
changeset 47729 44d1f4e0a46e
parent 47692 3d76c81b5ed2
child 48829 6ed588c4f963
     1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 24 11:07:50 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 24 13:55:02 2012 +0100
     1.3 @@ -482,14 +482,6 @@
     1.4       | _ => false
     1.5     end
     1.6  
     1.7 -(*Given a list of "'a option", apply an ('a -> 'b) function to each
     1.8 -element s.t. the function is only applied if that element isn't NONE*)
     1.9 -fun map_opt f xs =
    1.10 -  map (fn x =>
    1.11 -    if is_some x then
    1.12 -       SOME (f (the x))
    1.13 -    else NONE) xs
    1.14 -
    1.15  (*
    1.16   Information needed to be carried around:
    1.17   - constant mapping: maps constant names to Isabelle terms with fully-qualified
    1.18 @@ -625,7 +617,7 @@
    1.19          let
    1.20            val var_types' =
    1.21                ListPair.unzip bindings
    1.22 -           |> (apsnd (map_opt (interpret_type config thy type_map)))
    1.23 +           |> (apsnd ((map o Option.map) (interpret_type config thy type_map)))
    1.24             |> ListPair.zip
    1.25             |> List.rev
    1.26            fun fold_bind f =