dropped dead code
authorhaftmann
Sun, 26 Feb 2012 21:43:57 +0100
changeset 46695 b779c3f21f05
parent 46694 0988b22e2626
child 46696 28a01ea3523a
dropped dead code
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);