src/Pure/Isar/proof_context.ML

   val standard_term_uncheck: Proof.context -> term list -> term list
   val goal_export: Proof.context -> Proof.context -> thm list -> thm list
   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 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
   val match_bind_cmd: bool -> (string list * string) list -> Proof.context ->

   (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
     NONE => error "Pattern match failed!"
   | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 
-(* bind_terms *)
-
-val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
-  ctxt
-  |> 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);
-
-
 (* 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 |> maybe_bind_terms (map drop_schematic (f ctxt ts));
+fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
+
+
+(* bind terms (non-schematic) *)
+
+fun cert_maybe_bind_term (xi, t) ctxt =
+  ctxt
+  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
+
+val cert_bind_term = cert_maybe_bind_term o apsnd SOME;
 
 
 (* match_bind *)
 
 local

       if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
       else 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')
+          |> fold cert_bind_term binds'
+        else ctxt' |> fold cert_bind_term binds');
   in (ts, ctxt'') end;
 
 in
 
 fun read_terms ctxt T =

     |> fold Variable.declare_term props
     |> tap (Variable.warn_extra_tfrees ctxt)
     |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
     |-> (fn premss =>
       auto_bind_facts props
-      #> bind_terms binds
+      #> fold Variable.bind_term binds
       #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
   end;
 
 in
 

 fun dest_cases ctxt =
   Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
   |> sort (int_ord o apply2 #1) |> map #2;
 
 local
+
+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 update_case _ _ ("", _) res = res
   | update_case _ _ (name, NONE) (cases, index) =
       (Name_Space.del_table name cases, index)
   | update_case context is_proper (name, SOME c) (cases, index) =

     val Rule_Cases.Case {fixes, ...} = c;
     val (ts, ctxt') = ctxt |> fold_map fix fixes;
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
-    |> maybe_bind_terms (map drop_schematic binds)
+    |> fold (cert_maybe_bind_term o drop_schematic) binds
     |> update_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;
 
 val apply_case = apfst fst oo case_result;