avoid unqualified exception;
authorwenzelm
Sun Jun 11 21:59:17 2006 +0200 (2006-06-11)
changeset 19841f2fa72c13186
parent 19840 600c35fd1b5e
child 19842 04120bdac80e
avoid unqualified exception;
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/toplevel.ML
src/Pure/Proof/reconstruct.ML
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Sun Jun 11 19:36:10 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun Jun 11 21:59:17 2006 +0200
     1.3 @@ -307,7 +307,7 @@
     1.4             \ nested recursion")
     1.5         | (SOME {index, descr, ...}) =>
     1.6             let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
     1.7 -               val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths =>
     1.8 +               val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
     1.9                   typ_error T ("Type constructor " ^ tname ^ " used with wrong\
    1.10                    \ number of arguments")
    1.11             in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Jun 11 19:36:10 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Jun 11 21:59:17 2006 +0200
     2.3 @@ -181,7 +181,7 @@
     2.4  fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
     2.5    | prep_var _ = NONE;
     2.6  
     2.7 -fun prep_inst (concl, xs) =	(*exception UnequalLengths *)
     2.8 +fun prep_inst (concl, xs) =	(*exception Library.UnequalLengths *)
     2.9    let val vs = InductAttrib.vars_of concl
    2.10    in List.mapPartial prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    2.11  
    2.12 @@ -199,7 +199,7 @@
    2.13  	    in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) 
    2.14  	    end
    2.15      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    2.16 -    val insts = List.concat (map prep_inst (concls ~~ varss)) handle UnequalLengths =>
    2.17 +    val insts = List.concat (map prep_inst (concls ~~ varss)) handle Library.UnequalLengths =>
    2.18        error (rule_name ^ " has different numbers of variables");
    2.19    in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
    2.20    i state;
     3.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Sun Jun 11 19:36:10 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sun Jun 11 21:59:17 2006 +0200
     3.3 @@ -54,7 +54,7 @@
     3.4  
     3.5  fun map3 _ [] [] [] = []
     3.6    | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
     3.7 -  | map3 _ _ _ _ = raise UnequalLengths;
     3.8 +  | map3 _ _ _ _ = raise Library.UnequalLengths;
     3.9  
    3.10  
    3.11  
    3.12 @@ -64,4 +64,4 @@
    3.13  
    3.14  
    3.15  fun the_single [x] = x
    3.16 -  | the_single _ = sys_error "the_single"
    3.17 \ No newline at end of file
    3.18 +  | the_single _ = sys_error "the_single"
     4.1 --- a/src/HOL/Tools/record_package.ML	Sun Jun 11 19:36:10 2006 +0200
     4.2 +++ b/src/HOL/Tools/record_package.ML	Sun Jun 11 21:59:17 2006 +0200
     4.3 @@ -664,7 +664,7 @@
     4.4                            val flds' = Sign.extern_const thy f :: map NameSpace.base fs;
     4.5                            val (args',more) = split_last args;
     4.6                           in (flds'~~args')@field_lst more end
     4.7 -                         handle UnequalLengths => [("",t)])
     4.8 +                         handle Library.UnequalLengths => [("",t)])
     4.9                     | NONE => [("",t)])
    4.10               | NONE => [("",t)])
    4.11         | _ => [("",t)])
    4.12 @@ -776,7 +776,7 @@
    4.13                                                  flds';
    4.14                                in flds''@field_lst more end
    4.15                                handle TYPE_MATCH     => [("",T)]
    4.16 -                                   | UnequalLengths => [("",T)])
    4.17 +                                   | Library.UnequalLengths => [("",T)])
    4.18                           | NONE => [("",T)])
    4.19                     | NONE => [("",T)])
    4.20               | NONE => [("",T)])
     5.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jun 11 19:36:10 2006 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jun 11 21:59:17 2006 +0200
     5.3 @@ -557,8 +557,8 @@
     5.4    | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
     5.5    | exn_msg true (THM (msg, i, thms)) =
     5.6        raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
     5.7 -  | exn_msg _ Option = raised "Option" []
     5.8 -  | exn_msg _ UnequalLengths = raised "UnequalLengths" []
     5.9 +  | exn_msg _ Option.Option = raised "Option" []
    5.10 +  | exn_msg _ Library.UnequalLengths = raised "UnequalLengths" []
    5.11    | exn_msg _ Empty = raised "Empty" []
    5.12    | exn_msg _ Subscript = raised "Subscript" []
    5.13    | exn_msg _ (Fail msg) = raised "Fail" [msg]
     6.1 --- a/src/Pure/Proof/reconstruct.ML	Sun Jun 11 19:36:10 2006 +0200
     6.2 +++ b/src/Pure/Proof/reconstruct.ML	Sun Jun 11 21:59:17 2006 +0200
     6.3 @@ -149,7 +149,7 @@
     6.4                  NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
     6.5                | SOME Ts => (env, Ts));
     6.6              val prop'' = subst_TVars (map fst tvars @ map snd fmap ~~ Ts)
     6.7 -              (forall_intr_vfs prop') handle UnequalLengths =>
     6.8 +              (forall_intr_vfs prop') handle Library.UnequalLengths =>
     6.9                  error ("Wrong number of type arguments for " ^
    6.10                    quote (fst (get_name_tags [] prop prf)))
    6.11            in (prop'', change_type (SOME Ts) prf, [], env', vTs) end;