src/Pure/Isar/theory_target.ML
changeset 25311 aa750e3a581c
parent 25291 870455627720
child 25320 618247e82f3d
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Nov 06 13:12:52 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Nov 06 13:12:53 2007 +0100
     1.3 @@ -305,8 +305,8 @@
     1.4    | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
     1.5  
     1.6  fun init_ctxt (Target {target, is_locale, is_class}) =
     1.7 -  (if is_locale then Locale.init target else ProofContext.init) #>
     1.8 -  is_class ? Class.init target;
     1.9 +  if is_locale then if is_class then Class.init target
    1.10 +    else Locale.init target else ProofContext.init;
    1.11  
    1.12  fun init_lthy (ta as Target {target, ...}) =
    1.13    Data.put ta #>