# HG changeset patch
# User wenzelm
# Date 1138059803 -3600
# Node ID 9098c92a945f56a08afdeb37dee30eec792b8f10
# Parent  4a58895f704c5bf894b5424befc6c63566112e2d
added dest_all;

diff -r 4a58895f704c -r 9098c92a945f src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jan 23 18:20:48 2006 +0100
+++ b/src/Pure/logic.ML	Tue Jan 24 00:43:23 2006 +0100
@@ -9,6 +9,7 @@
 signature LOGIC =
 sig
   val is_all: term -> bool
+  val dest_all: term -> typ * term
   val mk_equals: term * term -> term
   val dest_equals: term -> term * term
   val is_equals: term -> bool
@@ -70,6 +71,10 @@
 fun is_all (Const ("all", _) $ _) = true
   | is_all _ = false;
 
+fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
+  | dest_all t = raise TERM ("dest_all", [t]);
+
+
 
 (** equality **)