src/HOL/Tools/Function/mutual.ML
changeset 33766 c679f05600cd
parent 33671 4b0f2599ed48
child 33855 cd8acf137c9c
     1.1 --- a/src/HOL/Tools/Function/mutual.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/mutual.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
     1.5            let
     1.6              val ((f, (_, f_defthm)), lthy') =
     1.7 -              Local_Theory.define ""
     1.8 +              Local_Theory.define
     1.9                  ((Binding.name fname, mixfix),
    1.10                    ((Binding.conceal (Binding.name (fname ^ "_def")), []),
    1.11                    Term.subst_bound (fsum, f_def))) lthy