# HG changeset patch # User wenzelm # Date 1150055957 -7200 # Node ID f2fa72c131864f37c6c2f336c661c5659bded84c # Parent 600c35fd1b5ec107e19ecd5a4b49beba799905c7 avoid unqualified exception; diff -r 600c35fd1b5e -r f2fa72c13186 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Sun Jun 11 19:36:10 2006 +0200 +++ b/src/HOL/Tools/datatype_aux.ML Sun Jun 11 21:59:17 2006 +0200 @@ -307,7 +307,7 @@ \ nested recursion") | (SOME {index, descr, ...}) => let val (_, vars, _) = (the o AList.lookup (op =) descr) index; - val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths => + val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths => typ_error T ("Type constructor " ^ tname ^ " used with wrong\ \ number of arguments") in (i + index, map (fn (j, (tn, args, cs)) => (i + j, diff -r 600c35fd1b5e -r f2fa72c13186 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Sun Jun 11 19:36:10 2006 +0200 +++ b/src/HOL/Tools/datatype_package.ML Sun Jun 11 21:59:17 2006 +0200 @@ -181,7 +181,7 @@ fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x) | prep_var _ = NONE; -fun prep_inst (concl, xs) = (*exception UnequalLengths *) +fun prep_inst (concl, xs) = (*exception Library.UnequalLengths *) let val vs = InductAttrib.vars_of concl in List.mapPartial prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end; @@ -199,7 +199,7 @@ in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) end val concls = HOLogic.dest_concls (Thm.concl_of rule); - val insts = List.concat (map prep_inst (concls ~~ varss)) handle UnequalLengths => + val insts = List.concat (map prep_inst (concls ~~ varss)) handle Library.UnequalLengths => error (rule_name ^ " has different numbers of variables"); in occs_in_prems (inst_tac insts rule) (map #2 insts) i end) i state; diff -r 600c35fd1b5e -r f2fa72c13186 src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Sun Jun 11 19:36:10 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Sun Jun 11 21:59:17 2006 +0200 @@ -54,7 +54,7 @@ fun map3 _ [] [] [] = [] | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs - | map3 _ _ _ _ = raise UnequalLengths; + | map3 _ _ _ _ = raise Library.UnequalLengths; @@ -64,4 +64,4 @@ fun the_single [x] = x - | the_single _ = sys_error "the_single" \ No newline at end of file + | the_single _ = sys_error "the_single" diff -r 600c35fd1b5e -r f2fa72c13186 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sun Jun 11 19:36:10 2006 +0200 +++ b/src/HOL/Tools/record_package.ML Sun Jun 11 21:59:17 2006 +0200 @@ -664,7 +664,7 @@ val flds' = Sign.extern_const thy f :: map NameSpace.base fs; val (args',more) = split_last args; in (flds'~~args')@field_lst more end - handle UnequalLengths => [("",t)]) + handle Library.UnequalLengths => [("",t)]) | NONE => [("",t)]) | NONE => [("",t)]) | _ => [("",t)]) @@ -776,7 +776,7 @@ flds'; in flds''@field_lst more end handle TYPE_MATCH => [("",T)] - | UnequalLengths => [("",T)]) + | Library.UnequalLengths => [("",T)]) | NONE => [("",T)]) | NONE => [("",T)]) | NONE => [("",T)]) diff -r 600c35fd1b5e -r f2fa72c13186 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sun Jun 11 19:36:10 2006 +0200 +++ b/src/Pure/Isar/toplevel.ML Sun Jun 11 21:59:17 2006 +0200 @@ -557,8 +557,8 @@ | exn_msg false (THM (msg, _, _)) = raised "THM" [msg] | exn_msg true (THM (msg, i, thms)) = raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms) - | exn_msg _ Option = raised "Option" [] - | exn_msg _ UnequalLengths = raised "UnequalLengths" [] + | exn_msg _ Option.Option = raised "Option" [] + | exn_msg _ Library.UnequalLengths = raised "UnequalLengths" [] | exn_msg _ Empty = raised "Empty" [] | exn_msg _ Subscript = raised "Subscript" [] | exn_msg _ (Fail msg) = raised "Fail" [msg] diff -r 600c35fd1b5e -r f2fa72c13186 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Sun Jun 11 19:36:10 2006 +0200 +++ b/src/Pure/Proof/reconstruct.ML Sun Jun 11 21:59:17 2006 +0200 @@ -149,7 +149,7 @@ NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) | SOME Ts => (env, Ts)); val prop'' = subst_TVars (map fst tvars @ map snd fmap ~~ Ts) - (forall_intr_vfs prop') handle UnequalLengths => + (forall_intr_vfs prop') handle Library.UnequalLengths => error ("Wrong number of type arguments for " ^ quote (fst (get_name_tags [] prop prf))) in (prop'', change_type (SOME Ts) prf, [], env', vTs) end;