Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/mutual.ML
changeset 33643 b275f26a638b
parent 33393 2240b0e7fa10
child 33671 4b0f2599ed48 
--- a/src/HOL/Tools/Function/mutual.ML	Thu Nov 12 21:59:35 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Thu Nov 12 22:02:11 2009 +0100
@@ -146,7 +146,7 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              LocalTheory.define Thm.internalK
+              LocalTheory.define ""
                 ((Binding.name fname, mixfix),
                   ((Binding.conceal (Binding.name (fname ^ "_def")), []),
                   Term.subst_bound (fsum, f_def))) lthy
isabelle