# HG changeset patch
# User haftmann
# Date 1162283351 -3600
# Node ID d9789a87825dd4d0c53490f8c06ca587d059fc80
# Parent  e8657a20a52f926b48d1f9081555e73b98ca4113
cleanup

diff -r e8657a20a52f -r d9789a87825d src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Tue Oct 31 09:29:08 2006 +0100
+++ b/src/Pure/Tools/codegen_consts.ML	Tue Oct 31 09:29:11 2006 +0100
@@ -21,7 +21,7 @@
     -> ((string (*theory name*) * thm) * typ list) option
   val disc_typ_of_classop: theory -> const -> typ
   val disc_typ_of_const: theory -> (const -> typ) -> const -> typ
-  val consts_of: theory -> term -> const list * (string * typ) list
+  val consts_of: theory -> term -> const list
   val read_const: theory -> string -> const
   val string_of_const: theory -> const -> string
   val raw_string_of_const: const -> string
@@ -126,8 +126,7 @@
   | disc_typ_of_const thy f const = f const;
 
 fun consts_of thy t =
-  fold_aterms (fn Const c => cons (norm_of_typ thy c, c) | _ => I) t []
-  |> split_list;
+  fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t []
 
 
 (* reading constants as terms *)
diff -r e8657a20a52f -r d9789a87825d src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Oct 31 09:29:08 2006 +0100
+++ b/src/Pure/library.ML	Tue Oct 31 09:29:11 2006 +0100
@@ -46,7 +46,6 @@
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
   val perhaps: ('a -> 'a option) -> 'a -> 'a
-  val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
 
   (*exceptions*)
   val try: ('a -> 'b) -> 'a -> 'b option
@@ -119,7 +118,6 @@
   val chop: int -> 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val nth: 'a list -> int -> 'a
-  val nth_update: int * 'a -> 'a list -> 'a list
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val nth_list: 'a list list -> int -> 'a list
   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
@@ -350,10 +348,6 @@
 
 fun perhaps f x = the_default x (f x);
 
-fun merge_opt _ (NONE, y) = y
-  | merge_opt _ (x, NONE) = x
-  | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
-
 
 (* exceptions *)
 
@@ -549,12 +543,6 @@
             | itr (x::l) = f(x, itr l)
       in  itr l  end;
 
-fun fold_index f =
-  let
-    fun fold_aux _ [] y = y
-      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
-  in fold_aux 0 end;
-
 fun foldl_map f =
   let
     fun fold_aux (x, []) = (x, [])
@@ -600,12 +588,6 @@
 
 fun nth_list xss i = nth xss i handle Subscript => [];
 
-(*update nth element*)
-fun nth_update (n, x) xs =
-  (case chop n xs of
-    (_, []) => raise Subscript
-  | (prfx, _ :: sffx') => prfx @ (x :: sffx'));
-
 fun nth_map 0 f (x :: xs) = f x :: xs
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
   | nth_map _ _ [] = raise Subscript;
@@ -616,6 +598,12 @@
       | mapp i (x :: xs) = f (i, x) :: mapp (i+1) xs
   in mapp 0 end;
 
+fun fold_index f =
+  let
+    fun fold_aux _ [] y = y
+      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
+  in fold_aux 0 end;
+
 val last_elem = List.last;
 
 (*rear decomposition*)