--- a/src/Pure/Tools/invoke.ML Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/Tools/invoke.ML Thu Dec 04 14:43:33 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Tools/invoke.ML
- ID: $Id$
Author: Makarius
Schematic invocation of locale expression in proof context.
@@ -8,9 +7,9 @@
signature INVOKE =
sig
val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
- (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
val invoke_i: string * attribute list -> Locale.expr -> term option list ->
- (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Invoke: INVOKE =
@@ -60,9 +59,9 @@
| NONE => Drule.termI)) params';
val propp =
- [((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
- ((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'),
- ((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')];
+ [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
+ ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'),
+ ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')];
fun after_qed results =
Proof.end_block #>
Proof.map_context (fn ctxt =>