--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Sun Sep 21 20:14:04 2014 +0200
@@ -55,7 +55,7 @@
fun interpretation_tests timeout ctxt probs =
List.app
(interpretation_test timeout ctxt)
- (List.map situate probs)
+ (map situate probs)
*}
ML {*
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sun Sep 21 20:14:04 2014 +0200
@@ -543,7 +543,7 @@
annotation) and use them in its reconstruction.
*)
val filter_deps =
- List.filter (fn {name, ...} =>
+ filter (fn {name, ...} =>
let
val role = node_info fms #role name
in role <> TPTP_Syntax.Role_Definition andalso
@@ -1277,7 +1277,7 @@
val pannot = get_pannot_of_prob thy prob_name
val goal =
#meta pannot
- |> List.filter (fn (_, info) =>
+ |> filter (fn (_, info) =>
#role info = TPTP_Syntax.Role_Conjecture)
in
if null (#meta pannot) then
@@ -1301,8 +1301,8 @@
(*Difference between the constants appearing between two terms, minus "ignore_consts"*)
fun new_consts_between t1 t2 =
- List.filter
- (fn n => not (List.exists (fn n' => n' = n) ignore_consts))
+ filter
+ (fn n => not (exists (fn n' => n' = n) ignore_consts))
(list_diff (consts_in t2) (consts_in t1))
(*Generate definition binding for an equation*)
@@ -1678,7 +1678,7 @@
let
val parent_nodes = parents_of_node fms n
in
- if List.exists (node_is_inference fms "split_conjecture") parent_nodes then
+ if exists (node_is_inference fms "split_conjecture") parent_nodes then
(([], [branch_id]), intermediate_thy) (*all related branches are to be deleted*)
else
list_prod [] parent_nodes (n :: ns)
@@ -1701,7 +1701,7 @@
end
else (intermediate_thy, NONE)
in
- if List.exists (node_is_inference fms "split_conjecture") parent_nodes then
+ if exists (node_is_inference fms "split_conjecture") parent_nodes then
(([], []), thy')
else
list_prod [] parent_nodes (n :: ns)
@@ -1736,7 +1736,7 @@
|> (fn (paths, branch_ids) =>
filter (fn (info, _) =>
case info of
- Coinconsistent branch_id => List.exists (fn x => x = branch_id) branch_ids
+ Coinconsistent branch_id => exists (fn x => x = branch_id) branch_ids
| _ => true) paths)
|> compute_paths thy'
end
@@ -1820,13 +1820,13 @@
else
let
val defn_equations =
- List.filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition) fms
+ filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition) fms
|> map (fn (node, _, t, _) =>
(node,
get_defn_components t
|> mk_bind_eq prob_name []))
val axioms =
- List.filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Axiom) fms
+ filter (fn (_, role, _, _) => role = TPTP_Syntax.Role_Axiom) fms
|> map (fn (node, _, t, _) =>
(node,
mk_bind_ax prob_name node t))
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Sun Sep 21 20:14:04 2014 +0200
@@ -100,7 +100,7 @@
(*List subtraction*)
fun list_diff l1 l2 =
- List.filter (fn x => List.all (fn y => x <> y) l2) l1
+ filter (fn x => forall (fn y => x <> y) l2) l1
val _ = @{assert}
(list_diff [1,2,3] [2,4] = [1, 3])
@@ -769,7 +769,7 @@
let
val hyps_conjoined =
fold (fn a => fn b =>
- b andalso (List.all (fn x => x) a)) hyp_results true
+ b andalso (forall (fn x => x) a)) hyp_results true
val concs_conjoined =
fold (fn a => fn b =>
b andalso a) conc_results true
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Sep 21 20:14:04 2014 +0200
@@ -775,7 +775,7 @@
else
map (strip_top_all_vars [] #> snd #> Logic.strip_horn #> snd) gls
(*Remove skolem-definition conclusion, to avoid wasting time analysing it*)
- |> List.filter (try_dest_Trueprop #> conc_is_skolem_def #> not)
+ |> filter (try_dest_Trueprop #> conc_is_skolem_def #> not)
(*There should only be a single goal*) (*FIXME this might not always be the case, in practice*)
(* |> tap (fn x => @{assert} (is_some (try the_single x))) *)
@@ -831,7 +831,7 @@
Term.add_frees lhs []
|> distinct (op =)
(*check to make sure that params' <= params*)
- val _ = @{assert} (List.all (member (op =) params) params')
+ val _ = @{assert} (forall (member (op =) params) params')
val skolem_const_ty =
let
val (skolem_const_prety, no_params) =
@@ -1407,7 +1407,7 @@
| _ => NONE
fun check_sublist sought_sublist opt_list =
- if List.all is_none opt_list then false
+ if forall is_none opt_list then false
else
fold_options opt_list
|> flat
@@ -1427,7 +1427,7 @@
| InnerLoopOnce l' =>
map sublist_of_inner_loop_once l
|> check_sublist l'
- | _ => List.exists (curry (op =) x) l
+ | _ => exists (curry (op =) x) l
end;
fun loop_can_feature loop_feats l =
@@ -2069,8 +2069,8 @@
else
case the (source_inf_opt node) of
TPTP_Proof.Inference (_, _, parent_inf) =>
- List.map TPTP_Proof.parent_name parent_inf
- |> List.filter (node_is_of_role role)
+ map TPTP_Proof.parent_name parent_inf
+ |> filter (node_is_of_role role)
|> (*FIXME currently definitions are not
included in the proof annotations, so
i'm using all the definitions available
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Sun Sep 21 20:14:04 2014 +0200
@@ -298,7 +298,7 @@
val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
in
#meta pannot
- |> List.filter (fn (_, info) =>
+ |> filter (fn (_, info) =>
#role info = TPTP_Syntax.Role_Conjecture)
|> hd
|> snd |> #fmla
--- a/src/HOL/Tools/ATP/atp_satallax.ML Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Sun Sep 21 20:14:04 2014 +0200
@@ -360,7 +360,7 @@
rule, ...}) =
let
val role' = role_of_tptp_string role
- val new_transformed = List.filter
+ val new_transformed = filter
(fn s => size s >=4 andalso not (is_special_satallax_rule s) andalso not
(member (op =) already_transformed s)) used_assumptions
in
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Sun Sep 21 20:14:04 2014 +0200
@@ -505,8 +505,8 @@
val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence)
- val helper_lemmas_needed = List.exists (snd #> snd #> fst #> is_some) sko_eq_facts
- orelse List.exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse
+ val helper_lemmas_needed = exists (snd #> snd #> fst #> is_some) sko_eq_facts
+ orelse exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse
is_some non_eq_consequence0
val helper_lines =
--- a/src/HOL/Tools/lin_arith.ML Sun Sep 21 19:53:50 2014 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sun Sep 21 20:14:04 2014 +0200
@@ -662,7 +662,7 @@
(* subgoal that has 'terms' as premises *)
fun negated_term_occurs_positively (terms : term list) : bool =
- List.exists
+ exists
(fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
member Envir.aeconv terms (Trueprop $ t)
| _ => false)