src/Pure/Tools/invoke.ML

--- a/src/Pure/Tools/invoke.ML	Fri Apr 13 10:00:04 2007 +0200
+++ b/src/Pure/Tools/invoke.ML	Fri Apr 13 10:01:43 2007 +0200
@@ -120,7 +120,7 @@
     "schematic invocation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
-      >> (fn (((name, expr), insts), fixes) =>
+      >> (fn (((name, expr), (insts, _)), fixes) =>
           Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
 
 val _ = OuterSyntax.add_parsers [invokeP];