# HG changeset patch
# User haftmann
# Date 1248101345 -7200
# Node ID bafffa63ebfd5bdb8a4903fe421767891739ea97
# Parent  1c14f77201d4fcc70c23aa06fecb1e77947658fa
dropped add_registration interface in locale

diff -r 1c14f77201d4 -r bafffa63ebfd src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Isar/class.ML	Mon Jul 20 16:49:05 2009 +0200
@@ -68,9 +68,8 @@
     val base_morph = inst_morph
       $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
       $> Element.satisfy_morphism (the_list wit);
-    val defs = these_defs thy sups;
-    val eq_morph = Element.eq_morphism thy defs;
-    val morph = base_morph $> eq_morph;
+    val eqs = these_defs thy sups;
+    val eq_morph = Element.eq_morphism thy eqs;
 
     (* assm_intro *)
     fun prove_assm_intro thm =
@@ -97,7 +96,7 @@
            ORELSE' Tactic.assume_tac));
     val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
 
-  in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
+  in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
 
 
 (* reading and processing class specifications *)
@@ -284,9 +283,8 @@
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
-    #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration (class, (morph, export_morph))
-    #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
+    #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
+       Locale.add_registration_eqs (class, base_morph) eqs export_morph
     #> register class sups params base_sort base_morph axiom assm_intro of_class))
     |> TheoryTarget.init (SOME class)
     |> pair class
diff -r 1c14f77201d4 -r bafffa63ebfd src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Jul 20 16:49:05 2009 +0200
@@ -68,9 +68,8 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  val add_registration: string * (morphism * morphism) -> theory -> theory
+  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val amend_registration: morphism -> string * morphism -> theory -> theory
-  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
@@ -295,8 +294,7 @@
 fun activate_declarations dep = Context.proof_map (fn context =>
   let
     val thy = Context.theory_of context;
-    val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
-  in context' end);
+  in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end);
 
 fun activate_facts dep context =
   let
@@ -346,11 +344,6 @@
 fun all_registrations thy = Registrations.get thy
   |> map reg_morph;
 
-fun add_registration (name, (base_morph, export)) thy =
-  roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
-    (name, base_morph) (get_idents (Context.Theory thy), thy)
-  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
-
 fun amend_registration morph (name, base_morph) thy =
   let
     val regs = map #1 (Registrations.get thy);
@@ -373,8 +366,10 @@
     val morph = if null eqns then proto_morph
       else proto_morph $> Element.eq_morphism thy eqns;
   in
-    thy
-    |> add_registration (dep, (morph, export))
+    (get_idents (Context.Theory thy), thy)
+    |> roundup thy (fn (dep', morph') =>
+        Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph)
+    |> snd
     |> Context.theory_map (activate_facts (dep, morph $> export))
   end;