1.1 --- a/src/Provers/trancl.ML	Mon Feb 22 11:57:33 2010 +0100
     1.2 +++ b/src/Provers/trancl.ML	Mon Feb 22 14:11:03 2010 +0100
     1.3 @@ -541,9 +541,11 @@
     1.4    val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
     1.5    val prfs = solveTrancl (prems, C);
     1.6   in
     1.7 -  Subgoal.FOCUS (fn {prems, ...} =>
     1.8 -    let val thms = map (prove thy rel prems) prfs
     1.9 -    in rtac (prove thy rel thms prf) 1 end) ctxt n st
    1.10 +  Subgoal.FOCUS (fn {prems, concl, ...} =>
    1.11 +    let
    1.12 +      val SOME (_, _, rel', _) = decomp (term_of concl);
    1.13 +      val thms = map (prove thy rel' prems) prfs
    1.14 +    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
    1.15   end
    1.16   handle Cannot => Seq.empty);
    1.17  
    1.18 @@ -558,9 +560,11 @@
    1.19    val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
    1.20    val prfs = solveRtrancl (prems, C);
    1.21   in
    1.22 -  Subgoal.FOCUS (fn {prems, ...} =>
    1.23 -    let val thms = map (prove thy rel prems) prfs
    1.24 -    in rtac (prove thy rel thms prf) 1 end) ctxt n st
    1.25 +  Subgoal.FOCUS (fn {prems, concl, ...} =>
    1.26 +    let
    1.27 +      val SOME (_, _, rel', _) = decomp (term_of concl);
    1.28 +      val thms = map (prove thy rel' prems) prfs
    1.29 +    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
    1.30   end
    1.31   handle Cannot => Seq.empty | Subscript => Seq.empty);
    1.32