tuned signature;

--- a/src/Pure/Isar/obtain.ML	Sun Jun 07 21:30:53 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 07 21:58:18 2015 +0200
@@ -289,7 +289,7 @@
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
           (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
             [(Thm.empty_binding, asms)])
-        |> Proof.bind_terms Auto_Bind.no_facts
+        |> Proof.map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
       end;
 
     val goal = Var (("guess", 0), propT);

--- a/src/Pure/Isar/proof.ML	Sun Jun 07 21:30:53 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Jun 07 21:58:18 2015 +0200
@@ -19,7 +19,6 @@
   val map_context_result : (context -> 'a * context) -> state -> 'a * state
   val map_contexts: (context -> context) -> state -> state
   val propagate_ml_env: state -> state
-  val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
@@ -221,7 +220,6 @@
 fun propagate_ml_env state = map_contexts
   (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
 
-val bind_terms = map_context o Proof_Context.bind_terms;
 val put_thms = map_context oo Proof_Context.put_thms;
 
 
@@ -771,7 +769,7 @@
   in
     state'
     |> assume assumptions
-    |> bind_terms Auto_Bind.no_facts
+    |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
     |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   end;
 

--- a/src/Pure/Isar/proof_context.ML	Sun Jun 07 21:30:53 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 07 21:58:18 2015 +0200
@@ -105,7 +105,8 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
-  val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
+  val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
+  val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val match_bind: bool -> (term list * term) list -> Proof.context -> term list * Proof.context
@@ -828,17 +829,19 @@
 
 (* bind_terms *)
 
-val bind_terms = fold (fn (xi, t) => fn ctxt =>
+val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
   ctxt
   |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
 
+val bind_terms = maybe_bind_terms o map (apsnd SOME);
+
 
 (* auto_bind *)
 
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
-fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f ctxt ts));
+fun auto_bind f ts ctxt = ctxt |> maybe_bind_terms (map drop_schematic (f ctxt ts));
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
@@ -863,12 +866,11 @@
     val binds' =
       if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
       else binds;
-    val binds'' = map (apsnd SOME) binds';
     val ctxt'' =
       tap (Variable.warn_extra_tfrees ctxt)
        (if gen then
-          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds''
-        else ctxt' |> bind_terms binds'');
+          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds'
+        else ctxt' |> bind_terms binds');
   in (ts, ctxt'') end;
 
 in
@@ -902,8 +904,8 @@
     val propss = map (map fst) args;
     fun gen_binds ctxt0 = ctxt0
       |> bind_terms (map #1 binds ~~
-          map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
-  in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end;
+          map Term.close_schematic_term (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
+  in ((propss, gen_binds), ctxt' |> bind_terms binds) end;
 
 in
 
@@ -1234,7 +1236,7 @@
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
-    |> bind_terms (map drop_schematic binds)
+    |> maybe_bind_terms (map drop_schematic binds)
     |> update_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;