diff -r 0c82e00ba63e -r 8c32a0160b0d src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -59,8 +59,7 @@
 
 fun cterm_from_metis ctxt sym_tab wrap tm =
   let val thy = Proof_Context.theory_of ctxt in
-    tm |> hol_term_from_metis MX sym_tab ctxt
-       |> wrap
+    tm |> hol_term_from_metis ctxt MX sym_tab |> wrap
        |> Syntax.check_term
               (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
        |> cterm_of thy