src/Pure/axclass.ML
changeset 33173 b8ca12f6681a
parent 33172 61ee96bc9895
child 33278 ba9f52f56356
     1.1 --- a/src/Pure/axclass.ML	Sun Oct 25 20:54:21 2009 +0100
     1.2 +++ b/src/Pure/axclass.ML	Sun Oct 25 21:35:46 2009 +0100
     1.3 @@ -305,7 +305,7 @@
     1.4    in
     1.5      thy
     1.6      |> Sign.mandatory_path name_inst
     1.7 -    |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     1.8 +    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
     1.9      |-> (fn const' as Const (c'', _) =>
    1.10        Thm.add_def false true
    1.11          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))