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;