src/Provers/trancl.ML
changeset 32283 3bebc195c124
parent 32277 ff1e59a15146
child 32285 ab9b66c2bbca
--- a/src/Provers/trancl.ML	Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Provers/trancl.ML	Thu Jul 30 12:20:43 2009 +0200
@@ -541,7 +541,7 @@
   val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)));
   val prfs = solveTrancl (prems, C);
  in
-  FOCUS (fn {prems, ...} =>
+  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
  end
@@ -558,7 +558,7 @@
   val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)));
   val prfs = solveRtrancl (prems, C);
  in
-  FOCUS (fn {prems, ...} =>
+  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
  end