Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified default binding;
authorwenzelm
Wed, 28 Oct 2009 16:27:48 +0100
changeset 33279 6b086276bbf7
parent 33278 ba9f52f56356
child 33280 e3eaeba6ae28
simplified default binding; conceal internal bindings;
src/HOL/Tools/Function/mutual.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/mutual.ML	Wed Oct 28 16:25:27 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Oct 28 16:27:48 2009 +0100
@@ -146,9 +146,9 @@
       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 ((Binding.name fname, mixfix),
-                                            ((Binding.name (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
-                              lthy
+              LocalTheory.define Thm.internalK
+                ((Binding.name fname, mixfix),
+                  (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy
           in
             (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
                          f=SOME f, f_defthm=SOME f_defthm },
isabelle