--- a/src/HOL/Nominal/nominal_primrec.ML Wed Apr 18 16:23:31 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Apr 18 21:30:14 2007 +0200
@@ -209,7 +209,7 @@
val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
val def_prop as _ $ _ $ t =
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), subst_bounds (rev (map Free frees), strip_abs_body t)) end;