# HG changeset patch
# User wenzelm
# Date 1238254276 -3600
# Node ID 2d2076300185fef1b321b104208690c9563bbf10
# Parent  1a9f93c1ed2283e864f63eaf9ee2c81836bd81de
replaced add_binds(_i) by bind_terms -- internal version only;

diff -r 1a9f93c1ed22 -r 2d2076300185 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Mar 28 16:30:09 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Mar 28 16:31:16 2009 +0100
@@ -294,7 +294,7 @@
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
           (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
-        |> Proof.add_binds_i AutoBind.no_facts
+        |> Proof.bind_terms AutoBind.no_facts
       end;
 
     val goal = Var (("guess", 0), propT);
diff -r 1a9f93c1ed22 -r 2d2076300185 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Mar 28 16:30:09 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 28 16:31:16 2009 +0100
@@ -17,7 +17,7 @@
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
   val map_contexts: (context -> context) -> state -> state
-  val add_binds_i: (indexname * term option) list -> 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
@@ -204,7 +204,7 @@
 
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
-val add_binds_i = map_context o ProofContext.add_binds_i;
+val bind_terms = map_context o ProofContext.bind_terms;
 val put_thms = map_context oo ProofContext.put_thms;
 
 
@@ -695,7 +695,7 @@
   in
     state'
     |> assume_i assumptions
-    |> add_binds_i AutoBind.no_facts
+    |> bind_terms AutoBind.no_facts
     |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
   end;
 
diff -r 1a9f93c1ed22 -r 2d2076300185 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 16:30:09 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 16:31:16 2009 +0100
@@ -70,8 +70,7 @@
   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 add_binds: (indexname * string option) list -> Proof.context -> Proof.context
-  val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
+  val bind_terms: (indexname * term option) 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 -> (string list * string) list -> Proof.context -> term list * Proof.context
@@ -775,7 +774,7 @@
 
 
 
-(** bindings **)
+(** term bindings **)
 
 (* simult_matches *)
 
@@ -785,28 +784,23 @@
   | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
 
 
-(* add_binds(_i) *)
-
-local
+(* bind_terms *)
 
-fun gen_bind prep (xi as (x, _), raw_t) ctxt =
+val bind_terms = fold (fn (xi, t) => fn ctxt =>
   ctxt
-  |> Variable.add_binds [(xi, Option.map (prep (set_mode mode_default ctxt)) raw_t)];
+  |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
 
-in
+
+(* 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;
 
-val add_binds = fold (gen_bind Syntax.read_term);
-val add_binds_i = fold (gen_bind cert_term);
+fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
 
-fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
 val auto_bind_goal = auto_bind AutoBind.goal;
 val auto_bind_facts = auto_bind AutoBind.facts;
 
-end;
-
 
 (* match_bind(_i) *)
 
@@ -831,8 +825,8 @@
     val ctxt'' =
       tap (Variable.warn_extra_tfrees ctxt)
        (if gen then
-          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> add_binds_i binds''
-        else ctxt' |> add_binds_i binds'');
+          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds''
+        else ctxt' |> bind_terms binds'');
   in (ts, ctxt'') end;
 
 in
@@ -868,8 +862,8 @@
 
     (*generalize result: context evaluated now, binds added later*)
     val gen = Variable.exportT_terms ctxt' ctxt;
-    fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds)));
-  in (ctxt' |> add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end;
+    fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
+  in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end;
 
 in
 
@@ -1221,7 +1215,7 @@
     val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
   in
     ctxt'
-    |> add_binds_i (map drop_schematic binds)
+    |> bind_terms (map drop_schematic binds)
     |> add_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;