# HG changeset patch
# User berghofe
# Date 1266844263 -3600
# Node ID 206e2f1759cccc407ee76d57a414d5ba2f4b22bb
# Parent  54ab4921f826386eb127226674dac672e61028e8
Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
contained variables bound by meta level quantifiers.

diff -r 54ab4921f826 -r 206e2f1759cc src/Provers/trancl.ML
--- 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);