--- a/src/Pure/Isar/proof_context.ML Tue Jun 09 16:42:17 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Jun 09 22:24:33 2015 +0200
@@ -105,8 +105,6 @@
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 ->
@@ -815,26 +813,23 @@
| 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
@@ -857,8 +852,10 @@
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
@@ -1161,7 +1158,7 @@
|> 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;
@@ -1182,6 +1179,9 @@
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)
@@ -1213,7 +1213,7 @@
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;