src/Pure/Isar/class.ML
changeset 30755 7ef503d216c2
parent 30585 6b2ba4666336
child 30764 3e3e7aa0cc7a
     1.1 --- a/src/Pure/Isar/class.ML	Sat Mar 28 12:48:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Mar 28 16:00:54 2009 +0100
     1.3 @@ -225,8 +225,9 @@
     1.4        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     1.5      val all_params = Locale.params_of thy class;
     1.6      val raw_params = (snd o chop (length supparams)) all_params;
     1.7 -    fun add_const (b, SOME raw_ty, _) thy =
     1.8 +    fun add_const ((raw_c, raw_ty), _) thy =
     1.9        let
    1.10 +        val b = Binding.name raw_c;
    1.11          val c = Sign.full_name thy b;
    1.12          val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
    1.13          val ty0 = Type.strip_sorts ty;