auto_bind_goal, auto_bind_facts;

--- a/src/Pure/Isar/proof_context.ML	Sat Jun 05 20:32:49 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 05 20:33:27 1999 +0200
@@ -39,6 +39,8 @@
   val match_binds_i: (term list * term) list -> context -> context
   val bind_propp: context * (string * string list) -> context * term
   val bind_propp_i: context * (term * term list) -> context * term
+  val auto_bind_goal: term -> context -> context
+  val auto_bind_facts: term list -> context -> context
   val thms_closure: context -> xstring -> thm list option
   val get_thm: context -> string -> thm
   val get_thms: context -> string -> thm list
@@ -562,6 +564,12 @@
 val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop);
 
 
+(* auto binds *)
+
+val auto_bind_goal = add_binds_i o AutoBind.goal;
+val auto_bind_facts = add_binds_i o AutoBind.facts;
+
+
 
 (** theorems **)
 
@@ -638,6 +646,7 @@
     val ths = map (fn th => ([th], [])) asms;
     val (ctxt'', (_, thms)) =
       ctxt'
+      |> auto_bind_facts props
       |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
 
     val ctxt''' =