# HG changeset patch
# User haftmann
# Date 1144332502 -7200
# Node ID a4fe025ecd907502630c2a4162d1289c4dda80bc
# Parent  59f08f67ed3ffc66c424c394088921d7a2308145
minor changes

diff -r 59f08f67ed3f -r a4fe025ecd90 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Thu Apr 06 16:07:44 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Thu Apr 06 16:08:22 2006 +0200
@@ -80,7 +80,7 @@
     val copy = I;
     val extend = I;
     fun merge _ (((g1, c1), f1), ((g2, c2), f2)) =
-      ((Graph.merge (op =) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (K false)) (c1, c2)),
+      ((Graph.merge (op =) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)),
        Symtab.merge (op =) (f1, f2));
     fun print thy ((gr, _), _) =
       let
@@ -318,16 +318,14 @@
 fun add_locale opn name expr body thy =
   thy
   |> Locale.add_locale opn name expr body
-  |> (fn ((_, ctxt), thy) => (ctxt, thy))
   ||>> `(fn thy => intro_incr thy name expr)
-  |-> (fn (ctxt, intro) => pair ((Sign.full_name thy name, intro), ctxt));
+  |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
 
 fun add_locale_i opn name expr body thy =
   thy
   |> Locale.add_locale_i opn name expr body
-  |> (fn ((_, ctxt), thy) => (ctxt, thy))
   ||>> `(fn thy => intro_incr thy name expr)
-  |-> (fn (ctxt, intro) => pair ((name, intro), ctxt));
+  |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
 
 fun add_axclass_i (name, supsort) axs thy =
   let
@@ -512,7 +510,7 @@
         fun get_c raw_def =
           (fst o Sign.cert_def pp o tap_def thy o snd) raw_def;
         val c_given = map get_c raw_defs;
-        fun eq_c ((c1, ty1), (c2, ty2)) =
+        fun eq_c ((c1 : string, ty1), (c2, ty2)) =
           let
             val ty1' = Type.varifyT ty1;
             val ty2' = Type.varifyT ty2;
@@ -525,10 +523,10 @@
          of [] => ()
           | cs => error ("superfluous definition(s) given for "
                     ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
-        val _ = case subtract eq_c c_given c_req
+        (*val _ = case subtract eq_c c_given c_req
          of [] => ()
           | cs => error ("no definition(s) given for "
-                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
+                    ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);*)
       in () end;
     fun check_defs1 raw_defs c_req thy =
       let