# HG changeset patch
# User wenzelm
# Date 1005510732 -3600
# Node ID a987beab002d7d0e62bf34e6e6c954ec5f818b48
# Parent  d51d50636332f27ad14fa357f0895fc24e79bde1
facts: multiple args;

diff -r d51d50636332 -r a987beab002d src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sun Nov 11 21:31:52 2001 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Sun Nov 11 21:32:12 2001 +0100
@@ -11,8 +11,8 @@
 
 signature AUTO_BIND =
 sig
-  val goal: Sign.sg -> term -> (indexname * term option) list
-  val facts: Sign.sg -> string -> term list -> (indexname * term option) list
+  val goal: Sign.sg -> term list -> (indexname * term option) list
+  val facts: Sign.sg -> term list -> (indexname * term option) list
   val thesisN: string
 end;
 
@@ -32,7 +32,7 @@
 
 (* goal *)
 
-fun goal sg prop = statement_binds sg thesisN prop;
+fun goal sg props = statement_binds sg thesisN (Library.last_elem props);
 
 
 (* facts *)
@@ -42,8 +42,8 @@
     _ $ t => Some (Term.list_abs (Logic.strip_params prop, t))
   | _ => None);
 
-fun facts _ _ [] = []
-  | facts sg name props =
+fun facts _ [] = []
+  | facts sg props =
       let val prop = Library.last_elem props
       in [(Syntax.dddot_indexname, get_arg sg prop)] @ statement_binds sg thisN prop end;