| changeset 24680 | 0d355aa59e67 |
| parent 24493 | d4380e9b287b |
| child 24707 | dfeb98f84e93 |
--- a/src/HOLCF/Tools/fixrec_package.ML Sun Sep 23 22:23:24 2007 +0200 +++ b/src/HOLCF/Tools/fixrec_package.ML Sun Sep 23 22:23:27 2007 +0200 @@ -23,7 +23,7 @@ fun legacy_infer_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); +fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); val fix_eq2 = thm "fix_eq2";