src/Pure/Isar/class.ML
 changeset 32113 bafffa63ebfd parent 31987 f4c7be4d684f child 32206 b2e93cda0be8
```     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
```