--- 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,
--- 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;
--- 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"
--- 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)])
--- 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]
--- 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;