changeset 25016 | 2bcac52d7abc |
parent 24977 | 9f98751c9628 |
child 25046 | 3d0137a59dcb |
--- a/src/HOL/Tools/function_package/mutual.ML Fri Oct 12 22:01:56 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Sat Oct 13 17:16:39 2007 +0200 @@ -184,7 +184,7 @@ fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = let val ((f, (_, f_defthm)), lthy') = - LocalTheory.def Thm.internalK ((fname, mixfix), + LocalTheory.define Thm.internalK ((fname, mixfix), ((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) lthy in