src/HOL/Tools/meson.ML

 sig
   val trace: bool Unsynchronized.ref
   val term_pair_of: indexname * (typ * 'a) -> term * 'a
   val flexflex_first_order: thm -> thm
   val size_of_subgoals: thm -> int
-  val estimated_num_clauses: Proof.context -> int -> term -> int
   val has_too_many_clauses: Proof.context -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
   val presimplify: thm -> thm
   val make_nnf: Proof.context -> thm -> thm

 (**** Operators for forward proof ****)
 
 
 (** First-order Resolution **)
 
-fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
 
 (*FIXME: currently does not "rename variables apart"*)
 fun first_order_resolve thA thB =
   (case

 fun flexflex_first_order th =
   case Thm.tpairs_of th of
       [] => th
     | pairs =>
         let val thy = theory_of_thm th
-            val (tyenv, tenv) =
+            val (_, tenv) =
               fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
             val t_pairs = map term_pair_of (Vartab.dest tenv)
             val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
         in  th'  end
         handle THM _ => th;

      | NONE => raise THM("forward_res", 0, [st])
   end;
 
 (*Are any of the logical connectives in "bs" present in the term?*)
 fun has_conns bs =
-  let fun has (Const(a,_)) = false
+  let fun has (Const _) = false
         | has (Const(@{const_name Trueprop},_) $ p) = has p
         | has (Const(@{const_name Not},_) $ p) = has p
         | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
         | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
         | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p

 
 
 (*** Removal of duplicate literals ***)
 
 (*Forward proof, passing extra assumptions as theorems to the tactic*)
-fun forward_res2 ctxt nf hyps st =
+fun forward_res2 nf hyps st =
   case Seq.pull
         (REPEAT
          (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
          st)
   of SOME(th,_) => th

 
 (*Remove duplicates in P|Q by assuming ~P in Q
   rls (initially []) accumulates assumptions of the form P==>False*)
 fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
     handle THM _ => tryres(th,rls)
-    handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2),
+    handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2),
                            [disj_FalseD1, disj_FalseD2, asm_rl])
     handle THM _ => th;
 
 (*Remove duplicate literals, if there are any*)
 fun nodups ctxt th =

     else th;
 
 
 (*** The basic CNF transformation ***)
 
-fun estimated_num_clauses ctxt bound t =
+fun estimated_num_clauses bound t =
  let
   fun sum x y = if x < bound andalso y < bound then x+y else bound
   fun prod x y = if x < bound andalso y < bound then x*y else bound
   
   (*Estimate the number of clauses in order to detect infeasible theorems*)

     | signed_nclauses _ _ = 1; (* literal *)
  in signed_nclauses true t end
 
 fun has_too_many_clauses ctxt t =
   let val max_cl = Config.get ctxt max_clauses in
-    estimated_num_clauses ctxt (max_cl + 1) t > max_cl
+    estimated_num_clauses (max_cl + 1) t > max_cl
   end
 
 (*Replaces universally quantified variables by FREE variables -- because
   assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
 local  

   else th;
 
 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   is a HOL disjunction.*)
 fun add_contras crules th hcs =
-  let fun rots (0,th) = hcs
+  let fun rots (0,_) = hcs
         | rots (k,th) = zero_var_indexes (make_horn crules th) ::
                         rots(k-1, assoc_right (th RS disj_comm))
   in case nliterals(prop_of th) of
         1 => th::hcs
       | n => rots(n, assoc_right th)

 (** Iterative deepening version **)
 
 (*This version does only one inference per call;
   having only one eq_assume_tac speeds it up!*)
 fun prolog_step_tac' horns =
-    let val (horn0s, hornps) = (*0 subgoals vs 1 or more*)
+    let val (horn0s, _) = (*0 subgoals vs 1 or more*)
             take_prefix Thm.no_prems horns
         val nrtac = net_resolve_tac horns
     in  fn i => eq_assume_tac i ORELSE
                 match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
                 ((assume_tac i APPEND nrtac i) THEN check_tac)