Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_set.ML
changeset 43278 1fbdcebb364b
parent 42795 66fcc9882784
child 44045 2814ff2a6e3e 
--- 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
isabelle