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