# HG changeset patch
# User wenzelm
# Date 1129327681 -7200
# Node ID a06b185a26d7d26950476118f1da781dde495504
# Parent  2fa4f9b547619e07b8c950ab7d3f0afe744e716e
added no_facts;

diff -r 2fa4f9b54761 -r a06b185a26d7 src/Pure/Isar/auto_bind.ML
--- 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;