diff -r 1fd31f859fc7 -r 1fbdcebb364b src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Jun 08 15:39:55 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Jun 08 15:56:57 2011 +0200
@@ -206,7 +206,7 @@
   | (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
       SOME (SOME (_, (arity, _))) =>
         (fold (infer_arities thy arities) (arity ~~ List.take (ts, length arity)) fs
-           handle Subscript => error "infer_arities: bad term")
+           handle General.Subscript => error "infer_arities: bad term")
     | _ => fold (infer_arities thy arities) (map (pair NONE) ts)
       (case optf of
          NONE => fs