# HG changeset patch # User wenzelm # Date 1006199198 -3600 # Node ID c4a2a0686238fd8c91671ee34e573138978ad1f0 # Parent 0760eda193c4c7ffb3ad29c00b8ea42611a40182 fixed comment; goal: unbind if multiple statements; diff -r 0760eda193c4 -r c4a2a0686238 src/Pure/Isar/auto_bind.ML --- a/src/Pure/Isar/auto_bind.ML Mon Nov 19 20:46:05 2001 +0100 +++ b/src/Pure/Isar/auto_bind.ML Mon Nov 19 20:46:38 2001 +0100 @@ -4,9 +4,6 @@ License: GPL (GNU GENERAL PUBLIC LICENSE) Logic specific patterns and automatic term bindings. - -Note: the current implementation is not quite 'generic', but works -fine with common object-logics (HOL, FOL, ZF etc.). *) signature AUTO_BIND = @@ -32,7 +29,8 @@ (* goal *) -fun goal sg props = statement_binds sg thesisN (Library.last_elem props); +fun goal sg [prop] = statement_binds sg thesisN prop + | goal _ _ = [((thesisN, 0), None)]; (* facts *)