src/HOL/Tools/meson.ML
changeset 33339 d41f77196338
parent 33317 b4534348b8fd
child 33832 cff42395c246
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4  
     1.5  (*Generate Horn clauses for all contrapositives of a clause. The input, th,
     1.6    is a HOL disjunction.*)
     1.7 -fun add_contras crules (th,hcs) =
     1.8 +fun add_contras crules th hcs =
     1.9    let fun rots (0,th) = hcs
    1.10          | rots (k,th) = zero_var_indexes (make_horn crules th) ::
    1.11                          rots(k-1, assoc_right (th RS disj_comm))
    1.12 @@ -443,9 +443,9 @@
    1.13  
    1.14  (*Use "theorem naming" to label the clauses*)
    1.15  fun name_thms label =
    1.16 -    let fun name1 (th, (k,ths)) =
    1.17 +    let fun name1 th (k, ths) =
    1.18            (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
    1.19 -    in  fn ths => #2 (List.foldr name1 (length ths, []) ths)  end;
    1.20 +    in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
    1.21  
    1.22  (*Is the given disjunction an all-negative support clause?*)
    1.23  fun is_negative th = forall (not o #1) (literals (prop_of th));
    1.24 @@ -491,9 +491,9 @@
    1.25      TRYALL_eq_assume_tac;
    1.26  
    1.27  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
    1.28 -fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
    1.29 +fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
    1.30  
    1.31 -fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
    1.32 +fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
    1.33  
    1.34  
    1.35  (*Negation Normal Form*)
    1.36 @@ -553,19 +553,19 @@
    1.37         (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
    1.38          skolemize_nnf_list ctxt ths);
    1.39  
    1.40 -fun add_clauses (th,cls) =
    1.41 +fun add_clauses th cls =
    1.42    let val ctxt0 = Variable.thm_context th
    1.43 -      val (cnfs,ctxt) = make_cnf [] th ctxt0
    1.44 +      val (cnfs, ctxt) = make_cnf [] th ctxt0
    1.45    in Variable.export ctxt ctxt0 cnfs @ cls end;
    1.46  
    1.47  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.48    The resulting clauses are HOL disjunctions.*)
    1.49 -fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
    1.50 +fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
    1.51  
    1.52  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    1.53  fun make_horns ths =
    1.54      name_thms "Horn#"
    1.55 -      (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
    1.56 +      (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
    1.57  
    1.58  (*Could simply use nprems_of, which would count remaining subgoals -- no
    1.59    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)