dropped add_registration interface in locale
authorhaftmann
Mon Jul 20 16:49:05 2009 +0200 (2009-07-20)
changeset 32113bafffa63ebfd
parent 32078 1c14f77201d4
child 32114 35084ad81bd4
dropped add_registration interface in locale
src/Pure/Isar/class.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Jul 20 09:52:09 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Jul 20 16:49:05 2009 +0200
     1.3 @@ -68,9 +68,8 @@
     1.4      val base_morph = inst_morph
     1.5        $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
     1.6        $> Element.satisfy_morphism (the_list wit);
     1.7 -    val defs = these_defs thy sups;
     1.8 -    val eq_morph = Element.eq_morphism thy defs;
     1.9 -    val morph = base_morph $> eq_morph;
    1.10 +    val eqs = these_defs thy sups;
    1.11 +    val eq_morph = Element.eq_morphism thy eqs;
    1.12  
    1.13      (* assm_intro *)
    1.14      fun prove_assm_intro thm =
    1.15 @@ -97,7 +96,7 @@
    1.16             ORELSE' Tactic.assume_tac));
    1.17      val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
    1.18  
    1.19 -  in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
    1.20 +  in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
    1.21  
    1.22  
    1.23  (* reading and processing class specifications *)
    1.24 @@ -284,9 +283,8 @@
    1.25      ||> Theory.checkpoint
    1.26      |-> (fn (param_map, params, assm_axiom) =>
    1.27         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    1.28 -    #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
    1.29 -       Locale.add_registration (class, (morph, export_morph))
    1.30 -    #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
    1.31 +    #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
    1.32 +       Locale.add_registration_eqs (class, base_morph) eqs export_morph
    1.33      #> register class sups params base_sort base_morph axiom assm_intro of_class))
    1.34      |> TheoryTarget.init (SOME class)
    1.35      |> pair class
     2.1 --- a/src/Pure/Isar/locale.ML	Mon Jul 20 09:52:09 2009 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Mon Jul 20 16:49:05 2009 +0200
     2.3 @@ -68,9 +68,8 @@
     2.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     2.5  
     2.6    (* Registrations and dependencies *)
     2.7 -  val add_registration: string * (morphism * morphism) -> theory -> theory
     2.8 +  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
     2.9    val amend_registration: morphism -> string * morphism -> theory -> theory
    2.10 -  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
    2.11    val add_dependency: string -> string * morphism -> morphism -> theory -> theory
    2.12  
    2.13    (* Diagnostic *)
    2.14 @@ -295,8 +294,7 @@
    2.15  fun activate_declarations dep = Context.proof_map (fn context =>
    2.16    let
    2.17      val thy = Context.theory_of context;
    2.18 -    val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
    2.19 -  in context' end);
    2.20 +  in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end);
    2.21  
    2.22  fun activate_facts dep context =
    2.23    let
    2.24 @@ -346,11 +344,6 @@
    2.25  fun all_registrations thy = Registrations.get thy
    2.26    |> map reg_morph;
    2.27  
    2.28 -fun add_registration (name, (base_morph, export)) thy =
    2.29 -  roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
    2.30 -    (name, base_morph) (get_idents (Context.Theory thy), thy)
    2.31 -  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
    2.32 -
    2.33  fun amend_registration morph (name, base_morph) thy =
    2.34    let
    2.35      val regs = map #1 (Registrations.get thy);
    2.36 @@ -373,8 +366,10 @@
    2.37      val morph = if null eqns then proto_morph
    2.38        else proto_morph $> Element.eq_morphism thy eqns;
    2.39    in
    2.40 -    thy
    2.41 -    |> add_registration (dep, (morph, export))
    2.42 +    (get_idents (Context.Theory thy), thy)
    2.43 +    |> roundup thy (fn (dep', morph') =>
    2.44 +        Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph)
    2.45 +    |> snd
    2.46      |> Context.theory_map (activate_facts (dep, morph $> export))
    2.47    end;
    2.48