1.1 --- a/src/Provers/trancl.ML	Sun Feb 26 21:26:28 2012 +0100
     1.2 +++ b/src/Provers/trancl.ML	Sun Feb 26 21:43:57 2012 +0100
     1.3 @@ -358,7 +358,7 @@
     1.4        let
     1.5     val _ = visited := u :: !visited
     1.6     val descendents =
     1.7 -       List.foldr (fn ((v,l),ds) => if been_visited v then ds
     1.8 +       List.foldr (fn ((v,_),ds) => if been_visited v then ds
     1.9              else v :: dfs_visit g v @ ds)
    1.10          [] (adjacent eq_comp g u)
    1.11     in  descendents end
    1.12 @@ -510,7 +510,6 @@
    1.13            )
    1.14            else processTranclEdges es;
    1.15     in processTranclEdges tranclEdges end )
    1.16 -| _ => raise Cannot
    1.17  
    1.18  
    1.19  fun solveTrancl (asms, concl) =
    1.20 @@ -537,7 +536,7 @@
    1.21    val thy = Proof_Context.theory_of ctxt;
    1.22    val Hs = Logic.strip_assums_hyp A;
    1.23    val C = Logic.strip_assums_concl A;
    1.24 -  val (rel, subgoals, prf) = mkconcl_trancl C;
    1.25 +  val (rel, _, prf) = mkconcl_trancl C;
    1.26  
    1.27    val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
    1.28    val prfs = solveTrancl (prems, C);
    1.29 @@ -556,7 +555,7 @@
    1.30    val thy = Proof_Context.theory_of ctxt;
    1.31    val Hs = Logic.strip_assums_hyp A;
    1.32    val C = Logic.strip_assums_concl A;
    1.33 -  val (rel, subgoals, prf) = mkconcl_rtrancl C;
    1.34 +  val (rel, _, prf) = mkconcl_rtrancl C;
    1.35  
    1.36    val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
    1.37    val prfs = solveRtrancl (prems, C);