auto_bind_goal, auto_bind_facts;
authorwenzelm
Sat Jun 05 20:33:27 1999 +0200 (1999-06-05)
changeset 67890e5a965de17a
parent 6788 6eaf6856ee4a
child 6790 0a39f22f847a
auto_bind_goal, auto_bind_facts;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jun 05 20:32:49 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jun 05 20:33:27 1999 +0200
     1.3 @@ -39,6 +39,8 @@
     1.4    val match_binds_i: (term list * term) list -> context -> context
     1.5    val bind_propp: context * (string * string list) -> context * term
     1.6    val bind_propp_i: context * (term * term list) -> context * term
     1.7 +  val auto_bind_goal: term -> context -> context
     1.8 +  val auto_bind_facts: term list -> context -> context
     1.9    val thms_closure: context -> xstring -> thm list option
    1.10    val get_thm: context -> string -> thm
    1.11    val get_thms: context -> string -> thm list
    1.12 @@ -562,6 +564,12 @@
    1.13  val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop);
    1.14  
    1.15  
    1.16 +(* auto binds *)
    1.17 +
    1.18 +val auto_bind_goal = add_binds_i o AutoBind.goal;
    1.19 +val auto_bind_facts = add_binds_i o AutoBind.facts;
    1.20 +
    1.21 +
    1.22  
    1.23  (** theorems **)
    1.24  
    1.25 @@ -638,6 +646,7 @@
    1.26      val ths = map (fn th => ([th], [])) asms;
    1.27      val (ctxt'', (_, thms)) =
    1.28        ctxt'
    1.29 +      |> auto_bind_facts props
    1.30        |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
    1.31  
    1.32      val ctxt''' =