--- a/src/Pure/Tools/invoke.ML Fri Dec 05 18:42:39 2008 +0100
+++ b/src/Pure/Tools/invoke.ML Fri Dec 05 18:43:42 2008 +0100
@@ -120,7 +120,7 @@
(K.tag_proof K.prf_goal)
(SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
>> (fn ((((name, atts), expr), (insts, _)), fixes) =>
- Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
+ Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
end;