--- a/src/HOL/Tools/primrec.ML Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Sun Sep 12 19:04:02 2010 +0200
@@ -196,8 +196,7 @@
val def_name = Thm.def_name (Long_Name.base_name fname);
val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
(list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
- val rhs = singleton (Syntax.check_terms ctxt)
- (Type_Infer.constrain varT raw_rhs);
+ val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;