# HG changeset patch
# User haftmann
# Date 1254909964 -7200
# Node ID aba29da80c1b6fb7b555e2a776d2c5f9b3515ea1
# Parent  5cab25b2dcf98149dbf48d18337d6ad45ffa7173
do not use Locale.add_registration_eqs any longer

diff -r 5cab25b2dcf9 -r aba29da80c1b src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Oct 07 09:44:03 2009 +0200
+++ b/src/Pure/Isar/class.ML	Wed Oct 07 12:06:04 2009 +0200
@@ -68,8 +68,7 @@
     val base_morph = inst_morph
       $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
       $> Element.satisfy_morphism (the_list wit);
-    val eqs = these_defs thy sups;
-    val eq_morph = Element.eq_morphism thy eqs;
+    val eq_morph = Element.eq_morphism thy (these_defs thy sups);
 
     (* assm_intro *)
     fun prove_assm_intro thm =
@@ -96,7 +95,7 @@
            ORELSE' Tactic.assume_tac));
     val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
 
-  in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
+  in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
 
 
 (* reading and processing class specifications *)
@@ -287,8 +286,9 @@
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
-    #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration_eqs (class, base_morph) eqs export_morph
+    #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
+       Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
+         (*FIXME should not modify base_morph, although admissible*)
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> TheoryTarget.init (SOME class)
     |> pair class