changeset 24493 | d4380e9b287b |
parent 24219 | e558fe311376 |
child 24508 | c8b82fec6447 |
--- a/src/Pure/Tools/nbe.ML Thu Aug 30 21:44:29 2007 +0200 +++ b/src/Pure/Tools/nbe.ML Thu Aug 30 22:35:34 2007 +0200 @@ -137,7 +137,7 @@ ^ 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