prefer explicitly qualified exception List.Empty;
authorwenzelm
Wed Mar 21 11:00:34 2012 +0100 (2012-03-21)
changeset 47060e2741ec9ae36
parent 47059 8e1b14bf0190
child 47061 355317493f34
prefer explicitly qualified exception List.Empty;
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Tools/Function/pat_completeness.ML
src/HOL/Tools/inductive_realizer.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/balanced_tree.ML
src/Pure/General/queue.ML
src/Pure/General/seq.ML
src/Pure/General/stack.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/proof.ML
src/Pure/Syntax/parser.ML
src/Pure/library.ML
src/Tools/induct.ML
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 20 21:37:31 2012 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Mar 21 11:00:34 2012 +0100
     1.3 @@ -341,7 +341,7 @@
     1.4    let
     1.5      fun default_prover_name () =
     1.6        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
     1.7 -      handle Empty => error "No ATP available."
     1.8 +      handle List.Empty => error "No ATP available."
     1.9      fun get_prover name =
    1.10        (name, Sledgehammer_Run.get_minimizing_prover ctxt
    1.11                  Sledgehammer_Provers.Normal name)
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 20 21:37:31 2012 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 21 11:00:34 2012 +0100
     2.3 @@ -83,7 +83,7 @@
     2.4     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
     2.5     rtac fs_name_thm 1 THEN
     2.6     etac exE 1) thm
     2.7 -  handle Empty  => all_tac thm (* if we collected no variables then we do nothing *)
     2.8 +  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
     2.9    end;
    2.10  
    2.11  fun get_inner_fresh_fun (Bound j) = NONE
     3.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Tue Mar 20 21:37:31 2012 +0100
     3.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Wed Mar 21 11:00:34 2012 +0100
     3.3 @@ -143,7 +143,7 @@
     3.4  
     3.5      val (qss, x_pats) = split_list (map pat_of cases)
     3.6      val xs = map fst (hd x_pats)
     3.7 -      handle Empty => raise COMPLETENESS
     3.8 +      handle List.Empty => raise COMPLETENESS
     3.9  
    3.10      val patss = map (map snd) x_pats
    3.11      val complete_thm = prove_completeness thy xs thesis qss patss
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Mar 20 21:37:31 2012 +0100
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Mar 21 11:00:34 2012 +0100
     4.3 @@ -505,7 +505,7 @@
     4.4        (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
     4.5             [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
     4.6           | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
     4.7 -         handle TERM _ => err () | Empty => err ();
     4.8 +         handle TERM _ => err () | List.Empty => err ();
     4.9    in 
    4.10      add_ind_realizers (hd sets)
    4.11        (case arg of
     5.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Mar 20 21:37:31 2012 +0100
     5.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 21 11:00:34 2012 +0100
     5.3 @@ -384,7 +384,7 @@
     5.4  fun extract_first p =
     5.5    let
     5.6      fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
     5.7 -      | extract xs [] = raise Empty
     5.8 +      | extract xs [] = raise List.Empty
     5.9    in extract [] end;
    5.10  
    5.11  fun print_ineqs ctxt ineqs =
     6.1 --- a/src/Pure/General/balanced_tree.ML	Tue Mar 20 21:37:31 2012 +0100
     6.2 +++ b/src/Pure/General/balanced_tree.ML	Wed Mar 21 11:00:34 2012 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4  structure Balanced_Tree: BALANCED_TREE =
     6.5  struct
     6.6  
     6.7 -fun make _ [] = raise Empty
     6.8 +fun make _ [] = raise List.Empty
     6.9    | make _ [x] = x
    6.10    | make f xs =
    6.11        let
    6.12 @@ -24,7 +24,7 @@
    6.13        in f (make f ps, make f qs) end;
    6.14  
    6.15  fun dest f n x =
    6.16 -  if n <= 0 then raise Empty
    6.17 +  if n <= 0 then raise List.Empty
    6.18    else if n = 1 then [x]
    6.19    else
    6.20      let
     7.1 --- a/src/Pure/General/queue.ML	Tue Mar 20 21:37:31 2012 +0100
     7.2 +++ b/src/Pure/General/queue.ML	Wed Mar 21 11:00:34 2012 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4    val is_empty: 'a T -> bool
     7.5    val content: 'a T -> 'a list
     7.6    val enqueue: 'a -> 'a T -> 'a T
     7.7 -  val dequeue: 'a T -> 'a * 'a T
     7.8 +  val dequeue: 'a T -> 'a * 'a T  (*exception List.Empty*)
     7.9  end;
    7.10  
    7.11  structure Queue: QUEUE =
    7.12 @@ -30,6 +30,6 @@
    7.13  
    7.14  fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
    7.15    | dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
    7.16 -  | dequeue (Queue ([], [])) = raise Empty;
    7.17 +  | dequeue (Queue ([], [])) = raise List.Empty;
    7.18  
    7.19  end;
     8.1 --- a/src/Pure/General/seq.ML	Tue Mar 20 21:37:31 2012 +0100
     8.2 +++ b/src/Pure/General/seq.ML	Wed Mar 21 11:00:34 2012 +0100
     8.3 @@ -167,7 +167,7 @@
     8.4  fun lift f xq y = map (fn x => f x y) xq;
     8.5  fun lifts f xq y = maps (fn x => f x y) xq;
     8.6  
     8.7 -fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
     8.8 +fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty);
     8.9  
    8.10  (*print a sequence, up to "count" elements*)
    8.11  fun print print_elem count =
     9.1 --- a/src/Pure/General/stack.ML	Tue Mar 20 21:37:31 2012 +0100
     9.2 +++ b/src/Pure/General/stack.ML	Wed Mar 21 11:00:34 2012 +0100
     9.3 @@ -13,7 +13,7 @@
     9.4    val map_top: ('a -> 'a) -> 'a T -> 'a T
     9.5    val map_all: ('a -> 'a) -> 'a T -> 'a T
     9.6    val push: 'a T -> 'a T
     9.7 -  val pop: 'a T -> 'a T      (*exception Empty*)
     9.8 +  val pop: 'a T -> 'a T      (*exception List.Empty*)
     9.9  end;
    9.10  
    9.11  structure Stack: STACK =
    9.12 @@ -34,6 +34,6 @@
    9.13  fun push (x, xs) = (x, x :: xs);
    9.14  
    9.15  fun pop (_, x :: xs) = (x, xs)
    9.16 -  | pop (_, []) = raise Empty;
    9.17 +  | pop (_, []) = raise List.Empty;
    9.18  
    9.19  end;
    10.1 --- a/src/Pure/Isar/local_defs.ML	Tue Mar 20 21:37:31 2012 +0100
    10.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Mar 21 11:00:34 2012 +0100
    10.3 @@ -173,7 +173,7 @@
    10.4  
    10.5  val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
    10.6  
    10.7 -fun trans_list _ _ [] = raise Empty
    10.8 +fun trans_list _ _ [] = raise List.Empty
    10.9    | trans_list trans ctxt (th :: raw_eqs) =
   10.10        (case filter_out is_trivial raw_eqs of
   10.11          [] => th
    11.1 --- a/src/Pure/Isar/proof.ML	Tue Mar 20 21:37:31 2012 +0100
    11.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 21 11:00:34 2012 +0100
    11.3 @@ -183,7 +183,7 @@
    11.4  fun open_block (State st) = State (Stack.push st);
    11.5  
    11.6  fun close_block (State st) = State (Stack.pop st)
    11.7 -  handle Empty => error "Unbalanced block parentheses";
    11.8 +  handle List.Empty => error "Unbalanced block parentheses";
    11.9  
   11.10  fun level (State st) = Stack.level st;
   11.11  
    12.1 --- a/src/Pure/Syntax/parser.ML	Tue Mar 20 21:37:31 2012 +0100
    12.2 +++ b/src/Pure/Syntax/parser.ML	Wed Mar 21 11:00:34 2012 +0100
    12.3 @@ -201,7 +201,7 @@
    12.4                              val tk_prods =
    12.5                                these
    12.6                                  (AList.lookup (op =) nt_prods
    12.7 -                                  (SOME (hd l_starts handle Empty => unknown_start)));
    12.8 +                                  (SOME (hd l_starts handle List.Empty => unknown_start)));
    12.9  
   12.10                              (*add_lambda is true if an existing production of the nt
   12.11                                produces lambda due to the new lambda NT l*)
    13.1 --- a/src/Pure/library.ML	Tue Mar 20 21:37:31 2012 +0100
    13.2 +++ b/src/Pure/library.ML	Wed Mar 21 11:00:34 2012 +0100
    13.3 @@ -328,7 +328,7 @@
    13.4  fun single x = [x];
    13.5  
    13.6  fun the_single [x] = x
    13.7 -  | the_single _ = raise Empty;
    13.8 +  | the_single _ = raise List.Empty;
    13.9  
   13.10  fun singleton f x = the_single (f [x]);
   13.11  
   13.12 @@ -372,12 +372,12 @@
   13.13  
   13.14  (*  (op @) [x1, ..., xn]  ===>  ((x1 @ x2) @ x3) ... @ xn
   13.15      for operators that associate to the left (TAIL RECURSIVE)*)
   13.16 -fun foldl1 f [] = raise Empty
   13.17 +fun foldl1 f [] = raise List.Empty
   13.18    | foldl1 f (x :: xs) = foldl f (x, xs);
   13.19  
   13.20  (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
   13.21      for n > 0, operators that associate to the right (not tail recursive)*)
   13.22 -fun foldr1 f [] = raise Empty
   13.23 +fun foldr1 f [] = raise List.Empty
   13.24    | foldr1 f l =
   13.25        let fun itr [x] = x
   13.26              | itr (x::l) = f(x, itr l)
   13.27 @@ -454,7 +454,7 @@
   13.28    in mapp 0 end;
   13.29  
   13.30  (*rear decomposition*)
   13.31 -fun split_last [] = raise Empty
   13.32 +fun split_last [] = raise List.Empty
   13.33    | split_last [x] = ([], x)
   13.34    | split_last (x :: xs) = apfst (cons x) (split_last xs);
   13.35  
    14.1 --- a/src/Tools/induct.ML	Tue Mar 20 21:37:31 2012 +0100
    14.2 +++ b/src/Tools/induct.ML	Wed Mar 21 11:00:34 2012 +0100
    14.3 @@ -104,12 +104,12 @@
    14.4  
    14.5  val mk_var = Net.encode_type o #2 o Term.dest_Var;
    14.6  
    14.7 -fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
    14.8 +fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty =>
    14.9    raise THM ("No variables in conclusion of rule", 0, [thm]);
   14.10  
   14.11  in
   14.12  
   14.13 -fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
   14.14 +fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
   14.15    raise THM ("No variables in major premise of rule", 0, [thm]);
   14.16  
   14.17  val left_var_concl = concl_var hd;
    15.1 --- a/src/Tools/subtyping.ML	Tue Mar 20 21:37:31 2012 +0100
    15.2 +++ b/src/Tools/subtyping.ML	Wed Mar 21 11:00:34 2012 +0100
    15.3 @@ -832,7 +832,7 @@
    15.4        "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi).";
    15.5  
    15.6      val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
    15.7 -      handle Empty => error ("Not a proper map function:" ^ err_str t);
    15.8 +      handle List.Empty => error ("Not a proper map function:" ^ err_str t);
    15.9  
   15.10      fun gen_arg_var ([], []) = []
   15.11        | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =