--- a/src/HOL/Nominal/nominal_primrec.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Aug 30 22:35:34 2007 +0200
@@ -211,7 +211,7 @@
list_comb (Const (rec_name, dummyT), fs @ [Free x]))
val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
val def_prop as _ $ _ $ t =
- 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), subst_bounds (rev (map Free frees), strip_abs_body t)) end;