src/HOL/Tools/recdef.ML

     val tcs =
       (case get_recdef thy name of
         NONE => error ("No recdef definition of constant: " ^ quote name)
       | SOME {tcs, ...} => tcs);
     val i = the_default 1 opt_i;
-    val tc = nth tcs (i - 1) handle Subscript =>
+    val tc = nth tcs (i - 1) handle General.Subscript =>
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
     Specification.theorem "" NONE (K I)
       (Binding.conceal (Binding.name bname), atts) []