# HG changeset patch
# User wenzelm
# Date 1160177464 -7200
# Node ID bc2669d5744d0d2e079a3b33b506c32dcfd54114
# Parent  95d24e8d117e90396149dbff1989af348e3972bd
moved the_single to Pure/library.ML;
tuned;

diff -r 95d24e8d117e -r bc2669d5744d src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Oct 07 01:31:03 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Oct 07 01:31:04 2006 +0200
@@ -65,7 +65,7 @@
 fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
 
 val dest_implies_list = 
-    split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
+    split_last o (unfold (can Logic.dest_implies) (fst o Logic.dest_implies) (snd o Logic.dest_implies) single)
 
 fun implies_elim_swp a b = implies_elim b a
 
@@ -92,10 +92,6 @@
   | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
 
 
-fun the_single [x] = x
-  | the_single _ = sys_error "the_single"
-
-
 (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
 fun replace_frees assoc =
     map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of