67 (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs)); |
67 (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs)); |
68 |
68 |
69 |
69 |
70 (* define *) |
70 (* define *) |
71 |
71 |
72 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
72 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params = |
73 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
73 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
74 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) |
74 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) |
75 #> pair (lhs, def)); |
75 #> pair (lhs, def)); |
76 |
76 |
77 fun class_foundation (ta as Target {target, ...}) |
77 fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params = |
78 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
78 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
79 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
|
80 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) |
79 #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) |
81 #> Class.const target ((b, mx), (type_params, lhs)) |
80 #> Class.const target ((b, mx), (#1 params, lhs)) |
82 #> pair (lhs, def)); |
81 #> pair (lhs, def)); |
83 |
82 |
84 fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
83 fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
85 if is_class then class_foundation ta |
84 if is_class then class_foundation ta |
86 else if is_locale then locale_foundation ta |
85 else if is_locale then locale_foundation ta |