no cleverness for instance parameters
authorhaftmann
Tue Sep 25 12:16:13 2007 +0200 (2007-09-25)
changeset 24701f8bfd592a6dc
parent 24700 291665d063e4
child 24702 f875049a13a1
no cleverness for instance parameters
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Sep 25 12:16:12 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 25 12:16:13 2007 +0200
     1.3 @@ -216,11 +216,11 @@
     1.4    let
     1.5      val ((lhs as Const (c, ty), args), rhs) =
     1.6        (apfst Term.strip_comb o Logic.dest_equals) prop;
     1.7 -    fun add_inst' def ([], (Const (c_inst, ty))) =
     1.8 +    fun (*add_inst' def ([], (Const (c_inst, ty))) =
     1.9            if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
    1.10            then add_inst (c, tyco) (c_inst, def)
    1.11            else add_inst_def (class, tyco) (c, ty)
    1.12 -      | add_inst' _ t = add_inst_def (class, tyco) (c, ty);
    1.13 +      |*) add_inst' _ t = add_inst_def (class, tyco) (c, ty);
    1.14    in
    1.15      thy
    1.16      |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute thy) atts)]