src/Pure/Tools/class_package.ML
changeset 19929 5c882c3e610b
parent 19928 cb8472f4c5fd
child 19953 2f54a51f1801
equal deleted inserted replaced
19928:cb8472f4c5fd 19929:5c882c3e610b
   396     #-> (fn (name_axclass, (_, ax_axioms)) =>
   396     #-> (fn (name_axclass, (_, ax_axioms)) =>
   397           fold (add_global_constraint v name_axclass) mapp_this
   397           fold (add_global_constraint v name_axclass) mapp_this
   398     #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this))
   398     #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this))
   399     #> prove_interpretation_i (NameSpace.base name_locale, [])
   399     #> prove_interpretation_i (NameSpace.base name_locale, [])
   400           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
   400           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
   401           ((ALLGOALS o resolve_tac) ax_axioms)
   401           ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   402     #> pair ctxt
   402     #> pair ctxt
   403     )))))
   403     )))))
   404   end;
   404   end;
   405 
   405 
   406 in
   406 in