# HG changeset patch
# User berghofe
# Date 1090253697 -7200
# Node ID 8049f217428e6c111d4948e057ce5081a8b0f9ce
# Parent  61a52739cd82a2379b1f80878415a9eef881f118
Added function dest_list.

diff -r 61a52739cd82 -r 8049f217428e src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon Jul 19 18:14:22 2004 +0200
+++ b/src/HOL/hologic.ML	Mon Jul 19 18:14:57 2004 +0200
@@ -78,6 +78,7 @@
   val dest_binum: term -> int
   val mk_bin: int -> term
   val mk_list: ('a -> term) -> typ -> 'a list -> term
+  val dest_list: term -> term list
 end;
 
 
@@ -340,4 +341,8 @@
       T --> Type ("List.list", [T]) --> Type ("List.list", [T])) $ f x $
         mk_list f T xs;
 
+fun dest_list (Const ("List.list.Nil", _)) = []
+  | dest_list (Const ("List.list.Cons", _) $ x $ xs) = x :: dest_list xs
+  | dest_list t = raise TERM ("dest_list", [t]);
+
 end;