added no_facts;

--- a/src/Pure/Isar/auto_bind.ML	Sat Oct 15 00:08:00 2005 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Sat Oct 15 00:08:01 2005 +0200
@@ -13,6 +13,7 @@
   val goal: theory -> term list -> (indexname * term option) list
   val cases: theory -> term list -> (string * RuleCases.T option) list
   val facts: theory -> term list -> (indexname * term option) list
+  val no_facts: (indexname * term option) list
 end;
 
 structure AutoBind: AUTO_BIND =
@@ -51,5 +52,6 @@
       let val prop = Library.last_elem props
       in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
 
+val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
 
 end;