clarified term bindings;

--- a/src/Pure/Isar/auto_bind.ML	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Tue Jun 09 11:51:05 2015 +0200
@@ -11,7 +11,7 @@
   val assmsN: string
   val goal: Proof.context -> term list -> (indexname * term option) list
   val facts: Proof.context -> term list -> (indexname * term option) list
-  val no_facts: (indexname * term option) list
+  val no_facts: indexname list
 end;
 
 structure Auto_Bind: AUTO_BIND =
@@ -47,6 +47,6 @@
       let val prop = List.last props
       in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
 
-val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
+val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
 
 end;

--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 11:51:05 2015 +0200
@@ -130,11 +130,9 @@
     val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
     val params = map Free (xs' ~~ Ts);
     val cparams = map (Thm.cterm_of params_ctxt) params;
-    val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
+    val binds' = map (apsnd (fold_rev Term.lambda_name (xs ~~ params))) binds;
 
-    (*abstracted term bindings*)
-    val abs_term = Term.close_schematic_term o fold_rev Term.lambda_name (xs ~~ params);
-    val binds' = map (apsnd abs_term) binds;
+    val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
     (*obtain statements*)
     val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
@@ -158,7 +156,7 @@
     state
     |> Proof.enter_forward
     |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
-    |> Proof.map_context (Proof_Context.bind_terms binds')
+    |> Proof.map_context (fold Variable.bind_term binds')
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume
@@ -297,7 +295,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.map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+        |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
       end;
 
     val goal = Var (("guess", 0), propT);

--- a/src/Pure/Isar/proof.ML	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 11:51:05 2015 +0200
@@ -769,7 +769,7 @@
   in
     state'
     |> assume assumptions
-    |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+    |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
     |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   end;
 
@@ -935,8 +935,9 @@
       |> Thm.cterm_of ctxt
       |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
     val statement = ((kind, pos), propss', Thm.term_of goal);
+    val binds' = map #1 binds ~~ Variable.export_terms goal_ctxt ctxt (map #2 binds);
     val after_qed' = after_qed |>> (fn after_local => fn results =>
-      map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
+      map_context (fold Variable.bind_term binds') #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)

--- a/src/Pure/Isar/proof_context.ML	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jun 09 11:51:05 2015 +0200
@@ -107,7 +107,6 @@
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
   val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
   val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
-  val export_bind_terms: (indexname * term) list -> Proof.context -> 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 ->
@@ -823,14 +822,10 @@
 
 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));
+  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
 
 val bind_terms = maybe_bind_terms o map (apsnd SOME);
 
-fun export_bind_terms binds ctxt ctxt0 =
-  let val ts0 = map Term.close_schematic_term (Variable.export_terms ctxt ctxt0 (map snd binds))
-  in bind_terms (map fst binds ~~ ts0) ctxt0 end;
-
 
 (* auto_bind *)
 

--- a/src/Pure/variable.ML	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/Pure/variable.ML	Tue Jun 09 11:51:05 2015 +0200
@@ -24,7 +24,9 @@
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
   val declare_thm: thm -> Proof.context -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
-  val bind_term: indexname * term option -> Proof.context -> Proof.context
+  val bind_term: indexname * term -> Proof.context -> Proof.context
+  val unbind_term: indexname -> Proof.context -> Proof.context
+  val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
@@ -274,12 +276,16 @@
 
 (** term bindings **)
 
-fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi)
-  | bind_term ((x, i), SOME t) =
-      let
-        val u = Term.close_schematic_term t;
-        val U = Term.fastype_of u;
-      in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
+fun bind_term ((x, i), t) =
+  let
+    val u = Term.close_schematic_term t;
+    val U = Term.fastype_of u;
+  in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
+
+val unbind_term = map_binds o Vartab.delete_safe;
+
+fun maybe_bind_term (xi, SOME t) = bind_term (xi, t)
+  | maybe_bind_term (xi, NONE) = unbind_term xi;
 
 fun expand_binds ctxt =
   let
@@ -638,9 +644,8 @@
 fun focus_subgoal i st =
   let
     val all_vars = Thm.fold_terms Term.add_vars st [];
-    val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
   in
-    fold bind_term no_binds #>
+    fold (unbind_term o #1) all_vars #>
     fold (declare_constraints o Var) all_vars #>
     focus_cterm (Thm.cprem_of st i)
   end;