# HG changeset patch
# User berghofe
# Date 973616104 -3600
# Node ID bd1d199fc58e99663db212f0b695301adba6d4fa
# Parent  42e6b8502d52e1611bff96f1cd3571f90b5ce790
Thm.dest_abs now takes an additional argument.

diff -r 42e6b8502d52 -r bd1d199fc58e TFL/dcterm.sml
--- a/TFL/dcterm.sml	Tue Nov 07 17:53:12 2000 +0100
+++ b/TFL/dcterm.sml	Tue Nov 07 17:55:04 2000 +0100
@@ -118,7 +118,7 @@
 *)
 
 fun dest_binder expected tm = 
-  dest_abs(dest_monop expected tm)
+  dest_abs None (dest_monop expected tm)
   handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);
 
 
@@ -171,7 +171,7 @@
 
 val strip_comb   = strip (swap o dest_comb)  (* Goes to the "left" *)
 val strip_imp    = rev2swap o strip dest_imp
-val strip_abs    = rev2swap o strip dest_abs
+val strip_abs    = rev2swap o strip (dest_abs None)
 val strip_forall = rev2swap o strip dest_forall
 val strip_exists = rev2swap o strip dest_exists