src/Provers/trancl.ML
changeset 35281 206e2f1759cc
parent 33063 4d462963a7db
child 36692 54b64d4ad524
--- a/src/Provers/trancl.ML	Mon Feb 22 11:57:33 2010 +0100
+++ b/src/Provers/trancl.ML	Mon Feb 22 14:11:03 2010 +0100
@@ -541,9 +541,11 @@
   val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
   val prfs = solveTrancl (prems, C);
  in
-  Subgoal.FOCUS (fn {prems, ...} =>
-    let val thms = map (prove thy rel prems) prfs
-    in rtac (prove thy rel thms prf) 1 end) ctxt n st
+  Subgoal.FOCUS (fn {prems, concl, ...} =>
+    let
+      val SOME (_, _, rel', _) = decomp (term_of concl);
+      val thms = map (prove thy rel' prems) prfs
+    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
  end
  handle Cannot => Seq.empty);
 
@@ -558,9 +560,11 @@
   val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
   val prfs = solveRtrancl (prems, C);
  in
-  Subgoal.FOCUS (fn {prems, ...} =>
-    let val thms = map (prove thy rel prems) prfs
-    in rtac (prove thy rel thms prf) 1 end) ctxt n st
+  Subgoal.FOCUS (fn {prems, concl, ...} =>
+    let
+      val SOME (_, _, rel', _) = decomp (term_of concl);
+      val thms = map (prove thy rel' prems) prfs
+    in rtac (prove thy rel' thms prf) 1 end) ctxt n st
  end
  handle Cannot => Seq.empty | Subscript => Seq.empty);