src/Pure/Isar/class.ML
changeset 32886 aba29da80c1b
parent 32850 d95a7fd00bd4
child 32970 fbd2bb2489a8
     1.1 --- a/src/Pure/Isar/class.ML	Wed Oct 07 09:44:03 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Oct 07 12:06:04 2009 +0200
     1.3 @@ -68,8 +68,7 @@
     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 eqs = these_defs thy sups;
     1.8 -    val eq_morph = Element.eq_morphism thy eqs;
     1.9 +    val eq_morph = Element.eq_morphism thy (these_defs thy sups);
    1.10  
    1.11      (* assm_intro *)
    1.12      fun prove_assm_intro thm =
    1.13 @@ -96,7 +95,7 @@
    1.14             ORELSE' Tactic.assume_tac));
    1.15      val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
    1.16  
    1.17 -  in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
    1.18 +  in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
    1.19  
    1.20  
    1.21  (* reading and processing class specifications *)
    1.22 @@ -287,8 +286,9 @@
    1.23      ||> Theory.checkpoint
    1.24      |-> (fn (param_map, params, assm_axiom) =>
    1.25         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    1.26 -    #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
    1.27 -       Locale.add_registration_eqs (class, base_morph) eqs export_morph
    1.28 +    #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
    1.29 +       Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
    1.30 +         (*FIXME should not modify base_morph, although admissible*)
    1.31      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.32      |> TheoryTarget.init (SOME class)
    1.33      |> pair class