tuned;
authorsultana
Tue Apr 24 13:55:02 2012 +0100 (2012-04-24)
changeset 4772944d1f4e0a46e
parent 47720 b11dac707c78
child 47730 15f4309bb9eb
tuned;
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
     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 =