--- 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