src/Pure/Isar/class_target.ML
changeset 29360 a5be60c3674e
parent 29358 efdfe5dfe008
child 29362 f9ded2d789b9
     1.1 --- a/src/Pure/Isar/class_target.ML	Mon Jan 05 15:37:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon Jan 05 15:55:04 2009 +0100
     1.3 @@ -72,23 +72,23 @@
     1.4  structure Old_Locale =
     1.5  struct
     1.6  
     1.7 -val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
     1.8 +val intro_locales_tac = Old_Locale.intro_locales_tac; (*already forked!*)
     1.9  
    1.10 -val interpretation = Locale.interpretation;
    1.11 -val interpretation_in_locale = Locale.interpretation_in_locale;
    1.12 -val get_interpret_morph = Locale.get_interpret_morph;
    1.13 -val Locale = Locale.Locale;
    1.14 -val extern = Locale.extern;
    1.15 -val intros = Locale.intros;
    1.16 -val dests = Locale.dests;
    1.17 -val init = Locale.init;
    1.18 -val Merge = Locale.Merge;
    1.19 -val parameters_of_expr = Locale.parameters_of_expr;
    1.20 -val empty = Locale.empty;
    1.21 -val cert_expr = Locale.cert_expr;
    1.22 -val read_expr = Locale.read_expr;
    1.23 -val parameters_of = Locale.parameters_of;
    1.24 -val add_locale = Locale.add_locale;
    1.25 +val interpretation = Old_Locale.interpretation;
    1.26 +val interpretation_in_locale = Old_Locale.interpretation_in_locale;
    1.27 +val get_interpret_morph = Old_Locale.get_interpret_morph;
    1.28 +val Locale = Old_Locale.Locale;
    1.29 +val extern = Old_Locale.extern;
    1.30 +val intros = Old_Locale.intros;
    1.31 +val dests = Old_Locale.dests;
    1.32 +val init = Old_Locale.init;
    1.33 +val Merge = Old_Locale.Merge;
    1.34 +val parameters_of_expr = Old_Locale.parameters_of_expr;
    1.35 +val empty = Old_Locale.empty;
    1.36 +val cert_expr = Old_Locale.cert_expr;
    1.37 +val read_expr = Old_Locale.read_expr;
    1.38 +val parameters_of = Old_Locale.parameters_of;
    1.39 +val add_locale = Old_Locale.add_locale;
    1.40  
    1.41  end;
    1.42  
    1.43 @@ -401,7 +401,7 @@
    1.44    end;
    1.45  
    1.46  fun default_intro_tac ctxt [] =
    1.47 -      intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE
    1.48 +      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] ORELSE
    1.49        Locale.intro_locales_tac true ctxt []
    1.50    | default_intro_tac _ _ = no_tac;
    1.51