# HG changeset patch
# User wenzelm
# Date 1392922539 -3600
# Node ID 7f428e08111b944710399ea81618ae21d402d83f
# Parent  47286c8477493b6bc8ba09aafc1e4558ec2dcc12
removed dead code;

diff -r 47286c847749 -r 7f428e08111b src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Thu Feb 20 19:52:43 2014 +0100
+++ b/src/Tools/coherent.ML	Thu Feb 20 19:55:39 2014 +0100
@@ -21,7 +21,6 @@
 signature COHERENT =
 sig
   val verbose: bool Unsynchronized.ref
-  val show_facts: bool Unsynchronized.ref
   val coherent_tac: Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end;
@@ -78,7 +77,7 @@
 val empty_env = (Vartab.empty, Vartab.empty);
 
 (* Find matcher that makes conjunction valid in given state *)
-fun valid_conj ctxt facts env [] = Seq.single (env, [])
+fun valid_conj _ _ env [] = Seq.single (env, [])
   | valid_conj ctxt facts env (t :: ts) =
       Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
         (valid_conj ctxt facts
@@ -107,7 +106,7 @@
   end;
 
 (* Check whether disjunction is valid in given state *)
-fun is_valid_disj ctxt facts [] = false
+fun is_valid_disj _ _ [] = false
   | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
       let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in
         (case Seq.pull (valid_conj ctxt facts empty_env
@@ -116,17 +115,11 @@
         | NONE => is_valid_disj ctxt facts ds)
       end;
 
-val show_facts = Unsynchronized.ref false;
-
 fun string_of_facts ctxt s facts =
   cat_lines
     (s :: map (Syntax.string_of_term ctxt)
       (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
 
-fun print_facts ctxt facts =
-  if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
-  else ();
-
 fun valid ctxt rules goal dom facts nfacts nparams =
   let
     val seq =
@@ -151,7 +144,7 @@
           | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))))
   end
 
-and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
+and valid_cases _ _ _ _ _ _ _ [] = SOME []
   | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
       let
         val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));