--- a/src/Pure/Isar/auto_bind.ML Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML Wed Jun 10 14:46:31 2015 +0200
@@ -8,6 +8,7 @@
sig
val thesisN: string
val thisN: string
+ val premsN: string
val assmsN: string
val abs_params: term -> term -> term
val goal: Proof.context -> term list -> (indexname * term option) list
@@ -23,6 +24,7 @@
val thesisN = "thesis";
val thisN = "this";
val assmsN = "assms";
+val premsN = "prems";
fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;