src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 58412 f65f11f4854c
parent 58411 e3d0354d2129
child 58941 f09dd46352ba
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Sep 21 19:53:50 2014 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Sep 21 20:14:04 2014 +0200
     1.3 @@ -775,7 +775,7 @@
     1.4        else
     1.5          map (strip_top_all_vars [] #> snd #> Logic.strip_horn #> snd) gls
     1.6          (*Remove skolem-definition conclusion, to avoid wasting time analysing it*)
     1.7 -        |> List.filter (try_dest_Trueprop #> conc_is_skolem_def #> not)
     1.8 +        |> filter (try_dest_Trueprop #> conc_is_skolem_def #> not)
     1.9          (*There should only be a single goal*) (*FIXME this might not always be the case, in practice*)
    1.10          (* |> tap (fn x => @{assert} (is_some (try the_single x))) *)
    1.11  
    1.12 @@ -831,7 +831,7 @@
    1.13                Term.add_frees lhs []
    1.14                |> distinct (op =)
    1.15              (*check to make sure that params' <= params*)
    1.16 -            val _ = @{assert} (List.all (member (op =) params) params')
    1.17 +            val _ = @{assert} (forall (member (op =) params) params')
    1.18              val skolem_const_ty =
    1.19                let
    1.20                  val (skolem_const_prety, no_params) =
    1.21 @@ -1407,7 +1407,7 @@
    1.22          | _ => NONE
    1.23  
    1.24      fun check_sublist sought_sublist opt_list =
    1.25 -      if List.all is_none opt_list then false
    1.26 +      if forall is_none opt_list then false
    1.27        else
    1.28          fold_options opt_list
    1.29          |> flat
    1.30 @@ -1427,7 +1427,7 @@
    1.31        | InnerLoopOnce l' =>
    1.32            map sublist_of_inner_loop_once l
    1.33            |> check_sublist l'
    1.34 -      | _ => List.exists (curry (op =) x) l
    1.35 +      | _ => exists (curry (op =) x) l
    1.36    end;
    1.37  
    1.38  fun loop_can_feature loop_feats l =
    1.39 @@ -2069,8 +2069,8 @@
    1.40              else
    1.41                case the (source_inf_opt node) of
    1.42                    TPTP_Proof.Inference (_, _, parent_inf) =>
    1.43 -                    List.map TPTP_Proof.parent_name parent_inf
    1.44 -                    |> List.filter (node_is_of_role role)
    1.45 +                    map TPTP_Proof.parent_name parent_inf
    1.46 +                    |> filter (node_is_of_role role)
    1.47                      |> (*FIXME currently definitions are not
    1.48                           included in the proof annotations, so
    1.49                           i'm using all the definitions available