Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
facts: multiple args;
authorwenzelm
Sun, 11 Nov 2001 21:32:12 +0100
changeset 12140 a987beab002d
parent 12139 d51d50636332
child 12141 d8445053eee0
facts: multiple args;
src/Pure/Isar/auto_bind.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle