# HG changeset patch
# User blanchet
# Date 1332200670 -3600
# Node ID 5248fae40f0983b41e191bd4fe3b0c1482891058
# Parent  77da780ddd6b489f8dab274954331e25bed1c743
tuning

diff -r 77da780ddd6b -r 5248fae40f09 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Mar 20 00:44:30 2012 +0100
@@ -349,10 +349,6 @@
   (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
 fun resop nf [prem] = resolve_tac (nf prem) 1;
 
-(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
-   and "Pure.term"? *)
-val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
-
 fun apply_skolem_theorem (th, rls) =
   let
     fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
@@ -423,39 +419,6 @@
     make_goal (tryres(th, clause_rules))
   handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
 
-(*Sort clauses by number of literals*)
-fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
-
-fun sort_clauses ths = sort (make_ord fewerlits) ths;
-
-fun has_bool @{typ bool} = true
-  | has_bool (Type (_, Ts)) = exists has_bool Ts
-  | has_bool _ = false
-
-fun has_fun (Type (@{type_name fun}, _)) = true
-  | has_fun (Type (_, Ts)) = exists has_fun Ts
-  | has_fun _ = false
-
-(*Is the string the name of a connective? Really only | and Not can remain,
-  since this code expects to be called on a clause form.*)
-val is_conn = member (op =)
-    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
-     @{const_name HOL.implies}, @{const_name Not},
-     @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
-
-(*True if the term contains a function--not a logical connective--where the type
-  of any argument contains bool.*)
-val has_bool_arg_const =
-    exists_Const
-      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
-
-(*A higher-order instance of a first-order constant? Example is the definition of
-  one, 1, at a function type in theory Function_Algebras.*)
-fun higher_inst_const thy (c,T) =
-  case binder_types T of
-      [] => false (*not a function type, OK*)
-    | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
-
 fun rigid t = not (is_Var (head_of t));
 
 fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
@@ -640,10 +603,13 @@
       val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0
   in Variable.export ctxt ctxt0 cnfs @ cls end;
 
+(*Sort clauses by number of literals*)
+fun fewerlits (th1, th2) = nliterals (prop_of th1) < nliterals (prop_of th2)
+
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
 fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths [];
-val make_clauses = sort_clauses oo make_clauses_unsorted;
+val make_clauses = sort (make_ord fewerlits) oo make_clauses_unsorted;
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =