--- 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;