src/Provers/trancl.ML

     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);
+ handle Cannot => Seq.empty | General.Subscript => Seq.empty);
 
 end;