changeset 22728 | ecbbdf50df2f |
parent 22692 | 1e057a3f087d |
child 23765 | 997e5fe47532 |
--- a/src/HOL/Tools/primrec_package.ML Wed Apr 18 16:23:31 2007 +0200 +++ b/src/HOL/Tools/primrec_package.ML Wed Apr 18 21:30:14 2007 +0200 @@ -204,7 +204,7 @@ val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; val def_prop = singleton (ProofContext.infer_types (ProofContext.init thy)) - (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1; + (Logic.mk_equals (Const (fname, dummyT), rhs)); in (def_name, def_prop) end;