70 (*temporary adaption code to mediate between old and new locale code*) |
70 (*temporary adaption code to mediate between old and new locale code*) |
71 |
71 |
72 structure Old_Locale = |
72 structure Old_Locale = |
73 struct |
73 struct |
74 |
74 |
75 val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*) |
75 val intro_locales_tac = Old_Locale.intro_locales_tac; (*already forked!*) |
76 |
76 |
77 val interpretation = Locale.interpretation; |
77 val interpretation = Old_Locale.interpretation; |
78 val interpretation_in_locale = Locale.interpretation_in_locale; |
78 val interpretation_in_locale = Old_Locale.interpretation_in_locale; |
79 val get_interpret_morph = Locale.get_interpret_morph; |
79 val get_interpret_morph = Old_Locale.get_interpret_morph; |
80 val Locale = Locale.Locale; |
80 val Locale = Old_Locale.Locale; |
81 val extern = Locale.extern; |
81 val extern = Old_Locale.extern; |
82 val intros = Locale.intros; |
82 val intros = Old_Locale.intros; |
83 val dests = Locale.dests; |
83 val dests = Old_Locale.dests; |
84 val init = Locale.init; |
84 val init = Old_Locale.init; |
85 val Merge = Locale.Merge; |
85 val Merge = Old_Locale.Merge; |
86 val parameters_of_expr = Locale.parameters_of_expr; |
86 val parameters_of_expr = Old_Locale.parameters_of_expr; |
87 val empty = Locale.empty; |
87 val empty = Old_Locale.empty; |
88 val cert_expr = Locale.cert_expr; |
88 val cert_expr = Old_Locale.cert_expr; |
89 val read_expr = Locale.read_expr; |
89 val read_expr = Old_Locale.read_expr; |
90 val parameters_of = Locale.parameters_of; |
90 val parameters_of = Old_Locale.parameters_of; |
91 val add_locale = Locale.add_locale; |
91 val add_locale = Old_Locale.add_locale; |
92 |
92 |
93 end; |
93 end; |
94 |
94 |
95 (*structure New_Locale = |
95 (*structure New_Locale = |
96 struct |
96 struct |
399 in |
399 in |
400 Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st |
400 Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st |
401 end; |
401 end; |
402 |
402 |
403 fun default_intro_tac ctxt [] = |
403 fun default_intro_tac ctxt [] = |
404 intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE |
404 intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] ORELSE |
405 Locale.intro_locales_tac true ctxt [] |
405 Locale.intro_locales_tac true ctxt [] |
406 | default_intro_tac _ _ = no_tac; |
406 | default_intro_tac _ _ = no_tac; |
407 |
407 |
408 fun default_tac rules ctxt facts = |
408 fun default_tac rules ctxt facts = |
409 HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE |
409 HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE |