# HG changeset patch
# User haftmann
# Date 1330289037 -3600
# Node ID b779c3f21f05cf22444b2d3a5140084f11c86bb6
# Parent  0988b22e262673ffd4a606b2d36da04b0e2d7ff1
dropped dead code

diff -r 0988b22e2626 -r b779c3f21f05 src/Provers/trancl.ML
--- a/src/Provers/trancl.ML	Sun Feb 26 21:26:28 2012 +0100
+++ b/src/Provers/trancl.ML	Sun Feb 26 21:43:57 2012 +0100
@@ -358,7 +358,7 @@
       let
    val _ = visited := u :: !visited
    val descendents =
-       List.foldr (fn ((v,l),ds) => if been_visited v then ds
+       List.foldr (fn ((v,_),ds) => if been_visited v then ds
             else v :: dfs_visit g v @ ds)
         [] (adjacent eq_comp g u)
    in  descendents end
@@ -510,7 +510,6 @@
           )
           else processTranclEdges es;
    in processTranclEdges tranclEdges end )
-| _ => raise Cannot
 
 
 fun solveTrancl (asms, concl) =
@@ -537,7 +536,7 @@
   val thy = Proof_Context.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
-  val (rel, subgoals, prf) = mkconcl_trancl C;
+  val (rel, _, prf) = mkconcl_trancl C;
 
   val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
   val prfs = solveTrancl (prems, C);
@@ -556,7 +555,7 @@
   val thy = Proof_Context.theory_of ctxt;
   val Hs = Logic.strip_assums_hyp A;
   val C = Logic.strip_assums_concl A;
-  val (rel, subgoals, prf) = mkconcl_rtrancl C;
+  val (rel, _, prf) = mkconcl_rtrancl C;
 
   val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
   val prfs = solveRtrancl (prems, C);