src/Pure/goals.ML

     (string * term) list -> (string * term) list -> theory -> theory
   val open_locale: xstring -> theory -> theory
   val close_locale: xstring -> theory -> theory
   val print_scope: theory -> unit
   val read_cterm: Sign.sg -> string * typ -> cterm
-  val setup: (theory -> theory) list
 end;
 
 structure Goals: GOALS =
 struct
 

     end;
 end;
 
 
 structure LocalesData = TheoryDataFun(LocalesArgs);
+val _ = Context.add_setup [LocalesData.init];
 val print_locales = LocalesData.print;
 
 
 (* access locales *)
 

             val nosyn = List.concat (map #nosyn locale_list);
             val str_list = (collect_consts sign) \\ nosyn
         in Sign.pretty_term sign o (const_ssubst_list str_list)
         end
     else Sign.pretty_term sign;
-
-
-(** locale theory setup **)
-
-val setup =
- [LocalesData.init];
 
 
 
 (*** Goal package ***)