# HG changeset patch
# User haftmann
# Date 1190715373 -7200
# Node ID f8bfd592a6dccd371a8fa8f027ad16d31fdf58c2
# Parent  291665d063e4a88c6ad2e55fb42065d8a9d08ca3
no cleverness for instance parameters

diff -r 291665d063e4 -r f8bfd592a6dc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Sep 25 12:16:12 2007 +0200
+++ b/src/Pure/Isar/class.ML	Tue Sep 25 12:16:13 2007 +0200
@@ -216,11 +216,11 @@
   let
     val ((lhs as Const (c, ty), args), rhs) =
       (apfst Term.strip_comb o Logic.dest_equals) prop;
-    fun add_inst' def ([], (Const (c_inst, ty))) =
+    fun (*add_inst' def ([], (Const (c_inst, ty))) =
           if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
           then add_inst (c, tyco) (c_inst, def)
           else add_inst_def (class, tyco) (c, ty)
-      | add_inst' _ t = add_inst_def (class, tyco) (c, ty);
+      |*) add_inst' _ t = add_inst_def (class, tyco) (c, ty);
   in
     thy
     |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute thy) atts)]