# HG changeset patch
# User wenzelm
# Date 1164128852 -3600
# Node ID 5313a4cc382343b58294169e86954af7f90d786c
# Parent  883337ea2f3bacecb1bd910a140c63292a2b4510
LocalTheory.notes/defs: proper kind;

diff -r 883337ea2f3b -r 5313a4cc3823 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 21 18:07:31 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 21 18:07:32 2006 +0100
@@ -410,9 +410,10 @@
       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))
-              |> Envir.beta_norm (* Fixme: LocalTheory.def does not work if not beta-normal *)
+              |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
           
-      val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
+      val ((f, (_, f_defthm)), lthy) =
+        LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
     in
       ((f, f_defthm), lthy)
     end
diff -r 883337ea2f3b -r 5313a4cc3823 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Nov 21 18:07:31 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Nov 21 18:07:32 2006 +0100
@@ -161,9 +161,10 @@
     let
       fun def ((MutualPart {fvar=(fname, fT), cargTs, pthA, pthR, f_def, ...}), (_, mixfix)) lthy =
           let
-            val ((f, (_, f_defthm)), lthy') = LocalTheory.def ((fname, mixfix),
-                                                               ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
-                                                              lthy
+            val ((f, (_, f_defthm)), lthy') =
+              LocalTheory.def Thm.internalK ((fname, mixfix),
+                                            ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
+                              lthy
           in
             (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def,
                          f=SOME f, f_defthm=SOME f_defthm },