src/Provers/quasi.ML

     let val thms = map (prove prems) prfs
     in rtac (prove thms prf) 1 end) ctxt n st
  end
  handle Contr p =>
     (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
-      handle Subscript => Seq.empty)
+      handle General.Subscript => Seq.empty)
   | Cannot => Seq.empty
-  | Subscript => Seq.empty);
+  | General.Subscript => Seq.empty);
 
 end;