Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/dcterm.sml
changeset 10418 bd1d199fc58e
parent 10015 8c16ec5ba62b 
--- 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
isabelle