# 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 *)