1.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4    | (u, ts) => (case Option.map (lookup_arity thy arities) (name_type_of u) of
     1.5        SOME (SOME (_, (arity, _))) =>
     1.6          (fold (infer_arities thy arities) (arity ~~ List.take (ts, length arity)) fs
     1.7 -           handle Subscript => error "infer_arities: bad term")
     1.8 +           handle General.Subscript => error "infer_arities: bad term")
     1.9      | _ => fold (infer_arities thy arities) (map (pair NONE) ts)
    1.10        (case optf of
    1.11           NONE => fs