src/Pure/Isar/class_declaration.ML
changeset 72505 974071d873ba
parent 71018 d32ed8927a42
child 72536 589645894305
equal deleted inserted replaced
72504:13032e920fea 72505:974071d873ba
   325     |> snd |> Local_Theory.exit_global
   325     |> snd |> Local_Theory.exit_global
   326     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
   326     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
   327     |-> (fn (param_map, params, assm_axiom) =>
   327     |-> (fn (param_map, params, assm_axiom) =>
   328        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
   328        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
   329     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
   329     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
   330        Locale.add_registration_theory
   330        Locale.add_registration_theory'
   331          {inst = (class, base_morph),
   331          {inst = (class, base_morph),
   332            mixin = Option.map (rpair true) eq_morph,
   332            mixin = Option.map (rpair true) eq_morph,
   333            export = export_morph}
   333            export = export_morph}
   334     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
   334     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
   335     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
   335     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))