replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

--- a/src/HOL/Tools/function_package/fundef_core.ML	Sat Sep 01 15:47:01 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Sat Sep 01 15:47:03 2007 +0200
@@ -479,7 +479,7 @@
       val f_def = 
           Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
                                 Abs ("y", ranT, G $ Bound 1 $ Bound 0))
-              |> ProofContext.cert_term lthy
+              |> Syntax.check_term lthy
 
       val ((f, (_, f_defthm)), lthy) =
         LocalTheory.def Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy