--- 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;