# HG changeset patch # User wenzelm # Date 1411323244 -7200 # Node ID f65f11f4854c4a8dfffceac79c4505f5a6f85c0b # Parent e3d0354d2129bc0d9229e153ebaaf5f48e2f538f more standard Isabelle/ML operations; diff -r e3d0354d2129 -r f65f11f4854c src/HOL/TPTP/TPTP_Interpret_Test.thy --- 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 {* diff -r e3d0354d2129 -r f65f11f4854c src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.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)) diff -r e3d0354d2129 -r f65f11f4854c src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- 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 diff -r e3d0354d2129 -r f65f11f4854c src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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 diff -r e3d0354d2129 -r f65f11f4854c src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- 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 diff -r e3d0354d2129 -r f65f11f4854c src/HOL/Tools/ATP/atp_satallax.ML --- 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 diff -r e3d0354d2129 -r f65f11f4854c src/HOL/Tools/ATP/atp_waldmeister.ML --- 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 = diff -r e3d0354d2129 -r f65f11f4854c src/HOL/Tools/lin_arith.ML --- 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)