102 |
102 |
103 fun class_foundation (ta as Target {target, ...}) |
103 fun class_foundation (ta as Target {target, ...}) |
104 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
104 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
105 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
105 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
106 #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
106 #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
107 #> class_target ta (Class.declare target ((b, mx), (type_params, lhs))) |
107 #> class_target ta (Class.const target ((b, mx), (type_params, lhs))) |
108 #> pair (lhs, def)) |
108 #> pair (lhs, def)) |
109 |
109 |
110 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
110 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
111 if is_class then class_foundation ta |
111 if is_class then class_foundation ta |
112 else if is_locale then locale_foundation ta |
112 else if is_locale then locale_foundation ta |