--- 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
--- 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 },