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 33671 4b0f2599ed48
parent 33643 b275f26a638b
child 33766 c679f05600cd 
--- a/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 20:41:29 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 21:11:15 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 ""
+              Local_Theory.define ""
                 ((Binding.name fname, mixfix),
                   ((Binding.conceal (Binding.name (fname ^ "_def")), []),
                   Term.subst_bound (fsum, f_def))) lthy
isabelle