# HG changeset patch
# User wenzelm
# Date 1332324034 -3600
# Node ID e2741ec9ae361ed647fec57a43c39def85d5d3f8
# Parent  8e1b14bf01905646f20c8dd47a677b33d2a4c3e9
prefer explicitly qualified exception List.Empty;

diff -r 8e1b14bf0190 -r e2741ec9ae36 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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)
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/HOL/Nominal/nominal_fresh_fun.ML
--- 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
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/HOL/Tools/Function/pat_completeness.ML
--- 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
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/HOL/Tools/inductive_realizer.ML
--- 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
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Provers/Arith/fast_lin_arith.ML
--- 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 =
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/balanced_tree.ML
--- 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
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/queue.ML
--- 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;
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/seq.ML
--- 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 =
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/stack.ML
--- 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;
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/Isar/local_defs.ML
--- 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
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/Isar/proof.ML
--- 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;
 
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/Syntax/parser.ML
--- 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*)
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/library.ML
--- 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);
 
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Tools/induct.ML
--- 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;
diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Tools/subtyping.ML
--- 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) =