src/HOL/Tools/meson.ML
changeset 35870 05f3af00cc7e
parent 35845 e5980f0ad025
parent 35869 cac366550624
child 36001 992839c4be90
     1.1 --- a/src/HOL/Tools/meson.ML	Mon Mar 22 09:54:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Mar 22 10:25:44 2010 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val make_nnf: Proof.context -> thm -> thm
     1.5    val skolemize: Proof.context -> thm -> thm
     1.6    val is_fol_term: theory -> term -> bool
     1.7 +  val make_clauses_unsorted: thm list -> thm list
     1.8    val make_clauses: thm list -> thm list
     1.9    val make_horns: thm list -> thm list
    1.10    val best_prolog_tac: (thm -> int) -> thm list -> tactic
    1.11 @@ -560,7 +561,8 @@
    1.12  
    1.13  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.14    The resulting clauses are HOL disjunctions.*)
    1.15 -fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
    1.16 +fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
    1.17 +val make_clauses = sort_clauses o make_clauses_unsorted;
    1.18  
    1.19  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    1.20  fun make_horns ths =