src/Pure/Isar/theory_target.ML
changeset 29360 a5be60c3674e
parent 29358 efdfe5dfe008
child 29393 172213e44992
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Jan 05 15:37:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Jan 05 15:55:04 2009 +0100
     1.3 @@ -24,19 +24,19 @@
     1.4  (* new locales *)
     1.5  
     1.6  fun locale_extern new_locale x = 
     1.7 -  if new_locale then NewLocale.extern x else Locale.extern x;
     1.8 +  if new_locale then Locale.extern x else Old_Locale.extern x;
     1.9  fun locale_add_type_syntax new_locale x =
    1.10 -  if new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.11 +  if new_locale then Locale.add_type_syntax x else Old_Locale.add_type_syntax x;
    1.12  fun locale_add_term_syntax new_locale x =
    1.13 -  if new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.14 +  if new_locale then Locale.add_term_syntax x else Old_Locale.add_term_syntax x;
    1.15  fun locale_add_declaration new_locale x =
    1.16 -  if new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
    1.17 +  if new_locale then Locale.add_declaration x else Old_Locale.add_declaration x;
    1.18  fun locale_add_thmss new_locale x =
    1.19 -  if new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
    1.20 +  if new_locale then Locale.add_thmss x else Old_Locale.add_thmss x;
    1.21  fun locale_init new_locale x =
    1.22 -  if new_locale then NewLocale.init x else Locale.init x;
    1.23 +  if new_locale then Locale.init x else Old_Locale.init x;
    1.24  fun locale_intern new_locale x =
    1.25 -  if new_locale then NewLocale.intern x else Locale.intern x;
    1.26 +  if new_locale then Locale.intern x else Old_Locale.intern x;
    1.27  
    1.28  (* context data *)
    1.29  
    1.30 @@ -334,7 +334,7 @@
    1.31  
    1.32  fun init_target _ NONE = global_target
    1.33    | init_target thy (SOME target) =
    1.34 -      make_target target (NewLocale.test_locale thy (NewLocale.intern thy target))
    1.35 +      make_target target (Locale.test_locale thy (Locale.intern thy target))
    1.36        true (Class_Target.is_class thy target) ([], [], []) [];
    1.37  
    1.38  fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
    1.39 @@ -384,7 +384,7 @@
    1.40  
    1.41  fun context "-" thy = init NONE thy
    1.42    | context target thy = init (SOME (locale_intern
    1.43 -      (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy;
    1.44 +      (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
    1.45  
    1.46  fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
    1.47  fun instantiation_cmd raw_arities thy =