--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Mar 21 11:00:34 2012 +0100
@@ -341,7 +341,7 @@
let
fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
- handle Empty => error "No ATP available."
+ handle List.Empty => error "No ATP available."
fun get_prover name =
(name, Sledgehammer_Run.get_minimizing_prover ctxt
Sledgehammer_Provers.Normal name)
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 21 11:00:34 2012 +0100
@@ -83,7 +83,7 @@
(cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
rtac fs_name_thm 1 THEN
etac exE 1) thm
- handle Empty => all_tac thm (* if we collected no variables then we do nothing *)
+ handle List.Empty => all_tac thm (* if we collected no variables then we do nothing *)
end;
fun get_inner_fresh_fun (Bound j) = NONE
--- a/src/HOL/Tools/Function/pat_completeness.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML Wed Mar 21 11:00:34 2012 +0100
@@ -143,7 +143,7 @@
val (qss, x_pats) = split_list (map pat_of cases)
val xs = map fst (hd x_pats)
- handle Empty => raise COMPLETENESS
+ handle List.Empty => raise COMPLETENESS
val patss = map (map snd) x_pats
val complete_thm = prove_completeness thy xs thesis qss patss
--- a/src/HOL/Tools/inductive_realizer.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Mar 21 11:00:34 2012 +0100
@@ -505,7 +505,7 @@
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
[_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
| xs => map (pred_of o fst o HOLogic.dest_imp) xs)
- handle TERM _ => err () | Empty => err ();
+ handle TERM _ => err () | List.Empty => err ();
in
add_ind_realizers (hd sets)
(case arg of
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Mar 21 11:00:34 2012 +0100
@@ -384,7 +384,7 @@
fun extract_first p =
let
fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
- | extract xs [] = raise Empty
+ | extract xs [] = raise List.Empty
in extract [] end;
fun print_ineqs ctxt ineqs =
--- a/src/Pure/General/balanced_tree.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/balanced_tree.ML Wed Mar 21 11:00:34 2012 +0100
@@ -15,7 +15,7 @@
structure Balanced_Tree: BALANCED_TREE =
struct
-fun make _ [] = raise Empty
+fun make _ [] = raise List.Empty
| make _ [x] = x
| make f xs =
let
@@ -24,7 +24,7 @@
in f (make f ps, make f qs) end;
fun dest f n x =
- if n <= 0 then raise Empty
+ if n <= 0 then raise List.Empty
else if n = 1 then [x]
else
let
--- a/src/Pure/General/queue.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/queue.ML Wed Mar 21 11:00:34 2012 +0100
@@ -11,7 +11,7 @@
val is_empty: 'a T -> bool
val content: 'a T -> 'a list
val enqueue: 'a -> 'a T -> 'a T
- val dequeue: 'a T -> 'a * 'a T
+ val dequeue: 'a T -> 'a * 'a T (*exception List.Empty*)
end;
structure Queue: QUEUE =
@@ -30,6 +30,6 @@
fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
| dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
- | dequeue (Queue ([], [])) = raise Empty;
+ | dequeue (Queue ([], [])) = raise List.Empty;
end;
--- a/src/Pure/General/seq.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/seq.ML Wed Mar 21 11:00:34 2012 +0100
@@ -167,7 +167,7 @@
fun lift f xq y = map (fn x => f x y) xq;
fun lifts f xq y = maps (fn x => f x y) xq;
-fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
+fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty);
(*print a sequence, up to "count" elements*)
fun print print_elem count =
--- a/src/Pure/General/stack.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/stack.ML Wed Mar 21 11:00:34 2012 +0100
@@ -13,7 +13,7 @@
val map_top: ('a -> 'a) -> 'a T -> 'a T
val map_all: ('a -> 'a) -> 'a T -> 'a T
val push: 'a T -> 'a T
- val pop: 'a T -> 'a T (*exception Empty*)
+ val pop: 'a T -> 'a T (*exception List.Empty*)
end;
structure Stack: STACK =
@@ -34,6 +34,6 @@
fun push (x, xs) = (x, x :: xs);
fun pop (_, x :: xs) = (x, xs)
- | pop (_, []) = raise Empty;
+ | pop (_, []) = raise List.Empty;
end;
--- a/src/Pure/Isar/local_defs.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/Isar/local_defs.ML Wed Mar 21 11:00:34 2012 +0100
@@ -173,7 +173,7 @@
val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
-fun trans_list _ _ [] = raise Empty
+fun trans_list _ _ [] = raise List.Empty
| trans_list trans ctxt (th :: raw_eqs) =
(case filter_out is_trivial raw_eqs of
[] => th
--- a/src/Pure/Isar/proof.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 21 11:00:34 2012 +0100
@@ -183,7 +183,7 @@
fun open_block (State st) = State (Stack.push st);
fun close_block (State st) = State (Stack.pop st)
- handle Empty => error "Unbalanced block parentheses";
+ handle List.Empty => error "Unbalanced block parentheses";
fun level (State st) = Stack.level st;
--- a/src/Pure/Syntax/parser.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/Syntax/parser.ML Wed Mar 21 11:00:34 2012 +0100
@@ -201,7 +201,7 @@
val tk_prods =
these
(AList.lookup (op =) nt_prods
- (SOME (hd l_starts handle Empty => unknown_start)));
+ (SOME (hd l_starts handle List.Empty => unknown_start)));
(*add_lambda is true if an existing production of the nt
produces lambda due to the new lambda NT l*)
--- a/src/Pure/library.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/library.ML Wed Mar 21 11:00:34 2012 +0100
@@ -328,7 +328,7 @@
fun single x = [x];
fun the_single [x] = x
- | the_single _ = raise Empty;
+ | the_single _ = raise List.Empty;
fun singleton f x = the_single (f [x]);
@@ -372,12 +372,12 @@
(* (op @) [x1, ..., xn] ===> ((x1 @ x2) @ x3) ... @ xn
for operators that associate to the left (TAIL RECURSIVE)*)
-fun foldl1 f [] = raise Empty
+fun foldl1 f [] = raise List.Empty
| foldl1 f (x :: xs) = foldl f (x, xs);
(* (op @) [x1, ..., xn] ===> x1 @ (x2 ... @ (x[n-1] @ xn))
for n > 0, operators that associate to the right (not tail recursive)*)
-fun foldr1 f [] = raise Empty
+fun foldr1 f [] = raise List.Empty
| foldr1 f l =
let fun itr [x] = x
| itr (x::l) = f(x, itr l)
@@ -454,7 +454,7 @@
in mapp 0 end;
(*rear decomposition*)
-fun split_last [] = raise Empty
+fun split_last [] = raise List.Empty
| split_last [x] = ([], x)
| split_last (x :: xs) = apfst (cons x) (split_last xs);
--- a/src/Tools/induct.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Tools/induct.ML Wed Mar 21 11:00:34 2012 +0100
@@ -104,12 +104,12 @@
val mk_var = Net.encode_type o #2 o Term.dest_Var;
-fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
+fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty =>
raise THM ("No variables in conclusion of rule", 0, [thm]);
in
-fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
+fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
raise THM ("No variables in major premise of rule", 0, [thm]);
val left_var_concl = concl_var hd;
--- a/src/Tools/subtyping.ML Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Tools/subtyping.ML Wed Mar 21 11:00:34 2012 +0100
@@ -832,7 +832,7 @@
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi).";
val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
- handle Empty => error ("Not a proper map function:" ^ err_str t);
+ handle List.Empty => error ("Not a proper map function:" ^ err_str t);
fun gen_arg_var ([], []) = []
| gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =