src/Pure/Tools/nbe.ML

     fun check_tvars t = if null (Term.term_tvars t) then t else
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Sign.string_of_term thy) t);
     val ty = type_of t;
     fun constrain t =
-      singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
+      singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
     val _ = ensure_funs thy funcgr t;
   in
     t
     |> tracing (fn t => "Input:\n" ^ Display.raw_string_of_term t)
     |> NBE_Eval.eval thy (!tab)