src/Pure/locale.ML
author wenzelm
Mon Nov 09 15:40:26 1998 +0100 (1998-11-09)
changeset 5838 a4122945d638
parent 5782 7559f116cb10
child 6022 259e4f2114e1
permissions -rw-r--r--
added metacuts_tac;
     1 (*  Title:      Pure/locale.ML
     2     ID:         $Id$
     3     Author:     Florian Kammueller, University of Cambridge
     4 
     5 Locales. The theory section 'locale' declarings constants, assumptions and
     6 definitions that have local scope.  Typical form is
     7 
     8     locale Locale_name =
     9       fixes   (*variables that are fixed in the locale's scope*)
    10 	v :: T
    11       assumes (*meta-hypothesis that hold in the locale*)
    12 	Asm_name "meta-formula"  
    13       defines (*local definitions of fixed variables in terms of others*)
    14 	v_def "v x == ...x..."
    15 
    16 TODO:
    17   - operations on locales: extension, renaming.
    18 *)
    19 
    20 signature BASIC_LOCALE =
    21 sig
    22   val print_locales: theory -> unit
    23   val print_goals: int -> thm -> unit
    24   val print_goals_marker: string -> int -> thm -> unit
    25 end;
    26 
    27 signature LOCALE =
    28 sig
    29   include BASIC_LOCALE
    30   val get_thm: theory -> xstring -> thm
    31   val get_thms: theory -> xstring -> thm list
    32   type locale
    33   val add_locale: bstring -> (string * string * mixfix) list ->
    34     (string * string) list -> (string * string) list -> theory -> theory
    35   val add_locale_i: bstring -> (string * typ * mixfix) list ->
    36     (string * term) list -> (string * term) list -> theory -> theory
    37   val open_locale: xstring -> theory -> theory
    38   val close_locale: theory -> theory
    39   val in_locale: term list -> Sign.sg -> bool
    40   val is_open_loc_sg: Sign.sg -> bool
    41   val is_open_loc: theory -> bool
    42   val read_cterm: Sign.sg -> string * typ -> cterm
    43   val get_scope: theory -> (string * locale) list
    44   val get_scope_sg: Sign.sg -> (string * locale) list
    45   val collect_consts: Sign.sg -> string list
    46   val setup: (theory -> theory) list
    47 end;
    48 
    49 structure Locale: LOCALE =
    50 struct
    51 
    52 
    53 (** type locale **)
    54 
    55 type locale =
    56  {consts: (string * typ) list,
    57   nosyn: string list,
    58   rules: (string * term) list,
    59   defs: (string * term) list,
    60   thms: (string * thm) list,
    61   defaults: (string * sort) list * (string * typ) list * string list};
    62 
    63 fun make_locale consts nosyn rules defs thms defaults =
    64   {consts = consts, nosyn = nosyn, rules = rules, defs = defs,
    65     thms = thms, defaults = defaults}: locale;
    66 
    67 fun pretty_locale sg (name, {consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
    68   let
    69     val prt_typ = Pretty.quote o Sign.pretty_typ sg;
    70     val prt_term = Pretty.quote o Sign.pretty_term sg;
    71 
    72     fun pretty_const (c, T) = Pretty.block
    73       [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
    74 
    75     fun pretty_axiom (a, t) = Pretty.block
    76       [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    77   in
    78     Pretty.big_list (name ^ " =")
    79      [Pretty.big_list "consts:" (map pretty_const consts),
    80       Pretty.big_list "rules:" (map pretty_axiom rules),
    81       Pretty.big_list "defs:" (map pretty_axiom defs)]
    82   end;
    83 
    84 
    85 
    86 (** theory data **)
    87 
    88 (* data kind 'Pure/locales' *)
    89 
    90 type locale_data =
    91   {space: NameSpace.T,
    92     locales: locale Symtab.table,
    93     scope: (string * locale) list ref};
    94 
    95 fun make_locale_data space locales scope =
    96   {space = space, locales = locales, scope = scope}: locale_data;
    97 
    98 structure LocalesArgs =
    99 struct
   100   val name = "Pure/locales";
   101   type T = locale_data;
   102 
   103   val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
   104   fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
   105   fun merge ({space = space1, locales = locales1, scope = _},
   106     {space = space2, locales = locales2, scope = _}) =
   107       make_locale_data (NameSpace.merge (space1, space2))
   108         (Symtab.merge (K true) (locales1, locales2))
   109         (ref []);
   110 
   111   fun print sg {space, locales, scope} =
   112     let
   113       fun extrn name =
   114         if ! long_names then name else NameSpace.extern space name;
   115       val locs = map (apfst extrn) (Symtab.dest locales);
   116       val scope_names = rev (map (extrn o fst) (! scope));
   117     in
   118       Pretty.writeln (Display.pretty_name_space ("locale name space", space));
   119       Pretty.writeln (Pretty.big_list "locales:" (map (pretty_locale sg) locs));
   120       Pretty.writeln (Pretty.strs ("current scope:" :: scope_names))
   121     end;
   122 end;
   123 
   124 
   125 structure LocalesData = TheoryDataFun(LocalesArgs);
   126 val print_locales = LocalesData.print;
   127 
   128 
   129 (* access locales *)
   130 
   131 fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
   132 
   133 val get_locale = get_locale_sg o Theory.sign_of;
   134 
   135 fun put_locale (name, locale) thy =
   136   let
   137     val {space, locales, scope} = LocalesData.get thy;
   138     val space' = NameSpace.extend (space, [name]);
   139     val locales' = Symtab.update ((name, locale), locales);
   140   in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
   141 
   142 fun lookup_locale thy xname =
   143   let
   144     val {space, locales, ...} = LocalesData.get thy;
   145     val name = NameSpace.intern space xname;
   146   in apsome (pair name) (get_locale thy name) end;
   147 
   148 
   149 (* access scope *)
   150 
   151 val get_scope_sg = ! o #scope o LocalesData.get_sg;
   152 
   153 val get_scope = get_scope_sg o Theory.sign_of;
   154 
   155 fun change_scope f thy =
   156   let val {scope, ...} = LocalesData.get thy
   157   in scope := f (! scope) end;
   158 
   159 
   160 
   161 (** scope operations **)
   162 
   163 (* change scope *)
   164 
   165 fun the_locale thy xname =
   166   (case lookup_locale thy xname of
   167     Some loc => loc
   168   | None => error ("Unknown locale " ^ quote xname));
   169 
   170 fun open_locale xname thy =
   171   (change_scope (cons (the_locale thy xname)) thy; thy);
   172 
   173 fun pop_locale [] = error "Currently no open locales"
   174   | pop_locale (_ :: locs) = locs;
   175 
   176 fun close_locale thy = (change_scope pop_locale thy; thy);
   177 
   178 
   179 (** functions for goals.ML **)
   180 
   181 (* in_locale: check if hyps (: term list) of a proof are contained in the
   182    (current) scope. This function is needed in prepare_proof. It needs to
   183    refer to the signature, because theory is not available in prepare_proof. *)
   184 
   185 fun in_locale hyps sg =
   186     let val cur_sc = get_scope_sg sg;
   187         val rule_lists = map (#rules o snd) cur_sc;
   188         val def_lists = map (#defs o snd) cur_sc;
   189         val rules = map snd (foldr (op union) (rule_lists, []));
   190         val defs = map snd (foldr (op union) (def_lists, []));
   191         val defnrules = rules @ defs;
   192     in
   193         hyps subset defnrules
   194     end;
   195 
   196 
   197 (* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
   198 fun is_open_loc_sg sign =
   199     let val cur_sc = get_scope_sg sign
   200     in not(null(cur_sc)) end;
   201 
   202 val is_open_loc = is_open_loc_sg o Theory.sign_of;
   203 
   204 
   205 (* get theorems *)
   206 
   207 fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
   208 
   209 fun get_thmx f get thy name =
   210   (case get_first (get_thm_locale name) (get_scope thy) of
   211     Some thm => f thm
   212   | None => get thy name);
   213 
   214 val get_thm = get_thmx I PureThy.get_thm;
   215 
   216 val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
   217 
   218 
   219 
   220 (** define locales **)
   221 
   222 (* prepare types *)
   223 
   224 fun read_typ sg (envT, s) =
   225   let
   226     fun def_sort (x, ~1) = assoc (envT, x)
   227       | def_sort _ = None;
   228     val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
   229   in (Term.add_typ_tfrees (T, envT), T) end;
   230 
   231 fun cert_typ sg (envT, raw_T) =
   232   let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
   233   in (Term.add_typ_tfrees (T, envT), T) end;
   234 
   235 
   236 (* prepare props *)
   237 
   238 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
   239 
   240 fun enter_term t (envS, envT, used) =
   241   (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
   242 
   243 fun read_axm sg ((envS, envT, used), (name, s)) =
   244   let
   245     fun def_sort (x, ~1) = assoc (envS, x)
   246       | def_sort _ = None;
   247     fun def_type (x, ~1) = assoc (envT, x)
   248       | def_type _ = None;
   249     val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
   250   in
   251     (enter_term t (envS, envT, used), t)
   252   end;
   253 
   254 
   255 fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
   256   let val (_, t) = Theory.cert_axm sg (name, raw_t)
   257   in (enter_term t (envS, envT, used), t) end;
   258 
   259 
   260 (* Locale.read_cterm: read in a string as a certified term, and respect the bindings
   261    that already exist for subterms. If no locale is open, this function is equal to
   262    Thm.read_cterm  *)
   263 
   264 fun read_cterm sign =
   265     let val cur_sc = get_scope_sg sign;
   266         val defaults = map (#defaults o snd) cur_sc;
   267         val envS = flat (map #1 defaults);
   268         val envT = flat (map #2 defaults);
   269         val used = flat (map #3 defaults);
   270         fun def_sort (x, ~1) = assoc (envS, x)
   271           | def_sort _ = None;
   272         fun def_type (x, ~1) = assoc (envT, x)
   273           | def_type _ = None;
   274     in (if (is_open_loc_sg sign)
   275         then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
   276         else Thm.read_cterm sign)
   277     end;
   278 
   279 (* basic functions needed for definitions and display *)
   280 (* collect all locale constants of a scope, i.e. a list of locales *)
   281 fun collect_consts sg =
   282     let val cur_sc = get_scope_sg sg;
   283         val locale_list = map snd cur_sc;
   284         val const_list = flat (map #consts locale_list)
   285     in map fst const_list end;
   286 
   287 (* filter out the Free's in a term *)
   288 fun list_frees t =
   289     case t of Const(c,T) => []
   290   | Var(v,T) => []
   291   | Free(v,T)=> [Free(v,T)]
   292   | Bound x  => []
   293   | Abs(a,T,u) => list_frees u
   294   | t1 $ t2  => (list_frees t1)  @ (list_frees t2);
   295 
   296 (* filter out all Free's in a term that are not contained
   297    in a list of strings. Used to prepare definitions. The list of strings
   298    will be the consts of the scope. We filter out the "free" Free's to be
   299    able to bind them *)
   300 fun difflist term clist =
   301     let val flist = list_frees term;
   302         fun builddiff [] sl = []
   303           | builddiff (t :: tl) sl =
   304             let val Free(v,T) = t
   305             in
   306                 if (v mem sl)
   307                 then builddiff tl sl
   308                 else t :: (builddiff tl sl)
   309             end;
   310     in distinct(builddiff flist clist) end;
   311 
   312 (* Bind a term with !! over a list of "free" Free's.
   313    To enable definitions like x + y == .... (without quantifier).
   314    Complications, because x and y have to be removed from defaults *)
   315 fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
   316     let val diffl = rev(difflist term clist);
   317         fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
   318           | abs_o (_ , _) = error ("Can't be: abs_over_free");
   319         val diffl' = map (fn (Free (s, T)) => s) diffl;
   320         val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
   321     in (defaults', (s, foldl abs_o (term, diffl))) end;
   322 
   323 (* assume a definition, i.e assume the cterm of a definiton term and then eliminate
   324    the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
   325 fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
   326 
   327 
   328 (* concrete syntax *)
   329 
   330 fun mark_syn c = "\\<^locale>" ^ c;
   331 
   332 fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
   333 
   334 
   335 (* add_locale *)
   336 
   337 fun gen_add_locale prep_typ prep_term bname raw_consts raw_rules raw_defs thy =
   338   let val sign = Theory.sign_of thy;
   339 
   340     val name = Sign.full_name sign bname;
   341 
   342 
   343     (* prepare locale consts *)
   344 
   345     fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
   346       let
   347         val c = Syntax.const_name raw_c raw_mx;
   348         val c_syn = mark_syn c;
   349         val mx = Syntax.fix_mixfix raw_c raw_mx;
   350         val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
   351           error ("The error(s) above occured in locale constant " ^ quote c);
   352         val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
   353       in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
   354 
   355     val (envS0, loc_consts_syn) = foldl_map prep_const ([], raw_consts);
   356     val loc_consts = map #1 loc_consts_syn;
   357     val loc_syn = map #2 loc_consts_syn;
   358     val nosyn = map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn);
   359     val loc_trfuns = mapfilter #3 loc_consts_syn;
   360 
   361 
   362     (* 1st stage: syntax_thy *)
   363 
   364     val syntax_thy =
   365       thy
   366       |> Theory.add_modesyntax_i ("", true) loc_syn
   367       |> Theory.add_trfuns ([], loc_trfuns, [], []);
   368 
   369     val syntax_sign = Theory.sign_of syntax_thy;
   370 
   371 
   372     (* prepare rules and defs *)
   373 
   374     fun prep_axiom (env, (a, raw_t)) =
   375       let
   376         val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
   377           error ("The error(s) above occured in locale rule / definition " ^ quote a);
   378       in (env', (a, t)) end;
   379 
   380     val ((envS1, envT1, used1), loc_rules) =
   381       foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
   382     val (defaults, loc_defs) = foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
   383 
   384     val old_loc_consts = collect_consts syntax_sign;
   385     val new_loc_consts = (map #1 loc_consts);
   386     val all_loc_consts = old_loc_consts @ new_loc_consts;
   387 
   388     val (defaults, loc_defs_terms) = foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
   389     val loc_defs_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
   390     val (defaults, loc_thms_terms) = foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
   391     val loc_thms = (map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) (loc_thms_terms)) 
   392                    @ loc_defs_thms;
   393 
   394 
   395     (* error messages *)        (* FIXME improve *)
   396 
   397     val err_dup_locale =
   398       if is_none (get_locale thy name) then []
   399       else ["Duplicate definition of locale " ^ quote name];
   400 
   401     (* check if definientes are locale constants (in the same locale, so no redefining!) *)
   402     val err_def_head =
   403       let fun peal_appl t = 
   404             case t of 
   405                  t1 $ t2 => peal_appl t1
   406                | Free(t) => t
   407                | _ => error ("a bad locale definition");
   408 	  fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
   409 	    | lhs _ = error ("an illegal definition");
   410           val defs = map lhs loc_defs;
   411           val check = defs subset loc_consts
   412       in if check then [] 
   413          else ["defined item not declared fixed in locale " ^ quote name]
   414       end; 
   415 
   416     (* check that variables on rhs of definitions are either fixed or on lhs *)
   417     val err_var_rhs = 
   418       let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
   419             let val varl1 = difflist d1 all_loc_consts;
   420                 val varl2 = difflist d2 all_loc_consts
   421             in t andalso (varl2 subset varl1)
   422             end
   423             | compare_var_sides (_,_) = error ("an illegal definition");
   424           val check = foldl compare_var_sides (true, loc_defs)
   425       in if check then []
   426          else ["nonfixed variable on right hand side of a locale definition in locale" ^ quote name]
   427       end;
   428 
   429     val errs = err_dup_locale @ err_def_head @ err_var_rhs;
   430   in
   431     if null errs then ()
   432     else error (cat_lines errs);
   433 
   434     syntax_thy
   435     |> put_locale (name, 
   436 		   make_locale loc_consts nosyn loc_thms_terms loc_defs_terms
   437 		               loc_thms defaults)
   438   end;
   439 
   440 
   441 val add_locale = gen_add_locale read_typ read_axm;
   442 val add_locale_i = gen_add_locale cert_typ cert_axm;
   443 
   444 (** print functions **)
   445 (* idea: substitute all locale contants (Free's) that are syntactical by their
   446          "real" constant representation (i.e. \\<^locale>constname).
   447    - function const_ssubst does this substitution
   448    - function Locale.pretty_term:
   449              if locale is open then do this substitution & then call Sign.pretty_term
   450              else call Sign.pretty_term
   451 *)
   452 (* substitutes all Free variables s in t by Const's s *)
   453 fun const_ssubst t s =
   454     case t  of
   455         Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
   456       | Const(c,T) => Const(c,T)
   457       | Var(v,T) => Var(v,T)
   458       | Bound x  => Bound x
   459       | Abs(a,T,u) => Abs(a,T, const_ssubst u s)
   460       | t1 $ t2  => const_ssubst t1 s $ const_ssubst t2 s;
   461 
   462 (* FIXME: improve: can be expressed with foldl *)
   463 fun const_ssubst_list [] t = t
   464   | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
   465 
   466 (* Locale.pretty_term *)
   467 fun pretty_term sign =
   468     if (is_open_loc_sg sign) then
   469         let val locale_list = map snd(get_scope_sg sign);
   470             val nosyn = flat (map #nosyn locale_list);
   471             val str_list = (collect_consts sign) \\ nosyn
   472         in Sign.pretty_term sign o (const_ssubst_list str_list)
   473         end
   474     else Sign.pretty_term sign;
   475 
   476 
   477 
   478 (** print_goals **)
   479 
   480 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
   481 
   482 local
   483 
   484   (* utils *)
   485 
   486   fun ins_entry (x, y) [] = [(x, [y])]
   487     | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   488         if x = x' then (x', y ins ys') :: pairs
   489         else pair :: ins_entry (x, y) pairs;
   490 
   491   fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
   492     | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
   493     | add_consts (Abs (_, _, t), env) = add_consts (t, env)
   494     | add_consts (_, env) = env;
   495 
   496   fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
   497     | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
   498     | add_vars (Abs (_, _, t), env) = add_vars (t, env)
   499     | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
   500     | add_vars (_, env) = env;
   501 
   502   fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
   503     | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   504     | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   505 
   506   fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   507   fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   508 
   509 
   510   (* prepare atoms *)
   511 
   512   fun consts_of t = sort_cnsts (add_consts (t, []));
   513   fun vars_of t = sort_idxs (add_vars (t, []));
   514   fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
   515 
   516 in
   517 
   518   fun print_goals_marker begin_goal maxgoals state =
   519     let
   520       val {sign, ...} = rep_thm state;
   521 
   522       val prt_term = pretty_term sign;
   523       val prt_typ = Sign.pretty_typ sign;
   524       val prt_sort = Sign.pretty_sort sign;
   525 
   526       fun prt_atoms prt prtT (X, xs) = Pretty.block
   527         [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   528           Pretty.brk 1, prtT X];
   529 
   530       fun prt_var (x, ~1) = prt_term (Syntax.free x)
   531         | prt_var xi = prt_term (Syntax.var xi);
   532 
   533       fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   534         | prt_varT xi = prt_typ (TVar (xi, []));
   535 
   536       val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   537       val prt_vars = prt_atoms prt_var prt_typ;
   538       val prt_varsT = prt_atoms prt_varT prt_sort;
   539 
   540 
   541       fun print_list _ _ [] = ()
   542         | print_list name prt lst = (writeln "";
   543             Pretty.writeln (Pretty.big_list name (map prt lst)));
   544 
   545       fun print_subgoals (_, []) = ()
   546         | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
   547             [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]));
   548               print_subgoals (n + 1, As));
   549 
   550       val print_ffpairs =
   551         print_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair);
   552 
   553       val print_consts = print_list "Constants:" prt_consts o consts_of;
   554       val print_vars = print_list "Variables:" prt_vars o vars_of;
   555       val print_varsT = print_list "Type variables:" prt_varsT o varsT_of;
   556 
   557 
   558       val {prop, ...} = rep_thm state;
   559       val (tpairs, As, B) = Logic.strip_horn prop;
   560       val ngoals = length As;
   561 
   562       fun print_gs (types, sorts) =
   563        (Pretty.writeln (prt_term B);
   564         if ngoals = 0 then writeln "No subgoals!"
   565         else if ngoals > maxgoals then
   566           (print_subgoals (1, take (maxgoals, As));
   567             writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   568         else print_subgoals (1, As);
   569 
   570         print_ffpairs tpairs;
   571 
   572         if types andalso ! show_consts then print_consts prop else ();
   573         if types then print_vars prop else ();
   574         if sorts then print_varsT prop else ());
   575     in
   576       setmp show_no_free_types true
   577         (setmp show_types (! show_types orelse ! show_sorts)
   578           (setmp show_sorts false print_gs))
   579      (! show_types orelse ! show_sorts, ! show_sorts)
   580   end;
   581 
   582   val print_goals = print_goals_marker "";
   583 
   584 end;
   585 
   586 
   587 
   588 (** locale theory setup **)
   589 
   590 val setup =
   591  [LocalesData.init];
   592 
   593 end;
   594 
   595 structure BasicLocale: BASIC_LOCALE = Locale;
   596 open BasicLocale;