admit unbinding;

--- a/src/Pure/Isar/auto_bind.ML	Sat Sep 25 13:06:59 1999 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Sat Sep 25 13:07:48 1999 +0200
@@ -7,8 +7,8 @@
 
 signature AUTO_BIND =
 sig
-  val goal: term -> (indexname * term) list
-  val facts: string -> term list -> (indexname * term) list
+  val goal: term -> (indexname * term option) list
+  val facts: string -> term list -> (indexname * term option) list
 end;
 
 structure AutoBind: AUTO_BIND =
@@ -23,8 +23,8 @@
     val parms = Logic.strip_params prop;
     fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
 
-    val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
-      (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
+    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
+      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
   in map (fn (s, t) => ((s, 0), t)) env end;
 
 fun goal prop = statement_binds ("thesis", prop);
@@ -33,9 +33,8 @@
 (* facts *)
 
 fun dddot_bind prop =
-  (case Logic.strip_imp_concl prop of
-    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
-  | _ => []);
+  [(Syntax.dddot_indexname,
+      case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
 
 fun facts _ [] = []
   | facts name props =