src/HOL/Tools/Function/function_core.ML
changeset 33766 c679f05600cd
parent 33671 4b0f2599ed48
child 33855 cd8acf137c9c
     1.1 --- a/src/HOL/Tools/Function/function_core.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -518,7 +518,7 @@
     1.4          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
     1.5        |> Syntax.check_term lthy
     1.6    in
     1.7 -    Local_Theory.define ""
     1.8 +    Local_Theory.define
     1.9        ((Binding.name (function_name fname), mixfix),
    1.10          ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
    1.11    end