--- a/src/Provers/order.ML Thu Jul 30 11:23:57 2009 +0200
+++ b/src/Provers/order.ML Thu Jul 30 12:20:43 2009 +0200
@@ -1235,12 +1235,12 @@
val prfs = gen_solve mkconcl thy (lesss, C);
val (subgoals, prf) = mkconcl decomp less_thms thy C;
in
- FOCUS (fn {prems = asms, ...} =>
+ Subgoal.FOCUS (fn {prems = asms, ...} =>
let val thms = map (prove (prems @ asms)) prfs
in rtac (prove thms prf) 1 end) ctxt n st
end
handle Contr p =>
- (FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
handle Subscript => Seq.empty)
| Cannot => Seq.empty
| Subscript => Seq.empty)