# HG changeset patch
# User wenzelm
# Date 1188654423 -7200
# Node ID 6c612357cf3d91a7d283412a667725b8290ef662
# Parent  23ee6b7788c23e553247d730b9774de8c6b99284
replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

diff -r 23ee6b7788c2 -r 6c612357cf3d src/HOL/Tools/function_package/fundef_core.ML
--- 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