diff -r f6d9e0e0b153 -r 1de908189869 src/Pure/Tools/invoke.ML
--- 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 =>