| changeset 24493 | d4380e9b287b |
| parent 23779 | 742be2833ccd |
| child 24680 | 0d355aa59e67 |
--- a/src/HOLCF/Tools/fixrec_package.ML Thu Aug 30 21:44:29 2007 +0200 +++ b/src/HOLCF/Tools/fixrec_package.ML Thu Aug 30 22:35:34 2007 +0200 @@ -21,7 +21,7 @@ (* legacy type inference *) fun legacy_infer_term thy t = - singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t); + singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);