# 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;