changeset 24493 | d4380e9b287b |
parent 23765 | 997e5fe47532 |
child 24624 | b8383b1bbae3 |
--- a/src/HOL/Tools/primrec_package.ML Thu Aug 30 21:44:29 2007 +0200 +++ b/src/HOL/Tools/primrec_package.ML Thu Aug 30 22:35:34 2007 +0200 @@ -227,7 +227,7 @@ fs @ map Bound (0 ::(length ls downto 1)))) val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; val def_prop = - singleton (ProofContext.infer_types (ProofContext.init thy)) + singleton (Syntax.check_terms (ProofContext.init thy)) (Logic.mk_equals (Const (fname, dummyT), rhs)); in (def_name, def_prop) end;