src/Pure/Tools/invoke.ML

     |> Seq.hd
   end;
 
 fun infer_terms ctxt =
   Syntax.check_terms ctxt o
-    (map (fn (t, T) => TypeInfer.constrain t (TypeInfer.paramify_vars T)));
+    (map (fn (t, T) => TypeInfer.constrain (TypeInfer.paramify_vars T) t));
 
 in
 
 fun invoke x =
   gen_invoke Attrib.attribute Locale.read_expr ProofContext.read_termTs ProofContext.add_fixes x;