1.1 --- a/src/Pure/Isar/calculation.ML Tue Apr 03 19:24:18 2007 +0200
1.2 +++ b/src/Pure/Isar/calculation.ML Tue Apr 03 19:24:19 2007 +0200
1.3 @@ -16,7 +16,8 @@
1.4 val symmetric: attribute
1.5 val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
1.6 val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
1.7 - val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
1.8 + val finally_: (thmref * Attrib.src list) list option -> bool ->
1.9 + Proof.state -> Proof.state Seq.seq
1.10 val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
1.11 val moreover: bool -> Proof.state -> Proof.state
1.12 val ultimately: bool -> Proof.state -> Proof.state
1.13 @@ -154,7 +155,7 @@
1.14
1.15 val also = calculate Proof.get_thmss false;
1.16 val also_i = calculate (K I) false;
1.17 -val finally = calculate Proof.get_thmss true;
1.18 +val finally_ = calculate Proof.get_thmss true;
1.19 val finally_i = calculate (K I) true;
1.20
1.21
2.1 --- a/src/Pure/Isar/isar_cmd.ML Tue Apr 03 19:24:18 2007 +0200
2.2 +++ b/src/Pure/Isar/isar_cmd.ML Tue Apr 03 19:24:19 2007 +0200
2.3 @@ -459,9 +459,9 @@
2.4 val print_locales = Toplevel.unknown_theory o
2.5 Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
2.6
2.7 -fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o
2.8 +fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o
2.9 Toplevel.keep (fn state =>
2.10 - Locale.print_locale (Toplevel.theory_of state) show_facts import body);
2.11 + Locale.print_locale (Toplevel.theory_of state) show_facts imports body);
2.12
2.13 fun print_registrations show_wits name = Toplevel.unknown_context o
2.14 Toplevel.keep (Toplevel.node_case
3.1 --- a/src/Pure/Isar/isar_syn.ML Tue Apr 03 19:24:18 2007 +0200
3.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Apr 03 19:24:19 2007 +0200
3.3 @@ -665,7 +665,7 @@
3.4 val finallyP =
3.5 OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
3.6 (K.tag_proof K.prf_chain)
3.7 - (calc_args >> (Toplevel.proofs' o Calculation.finally));
3.8 + (calc_args >> (Toplevel.proofs' o Calculation.finally_));
3.9
3.10 val moreoverP =
3.11 OuterSyntax.command "moreover" "augment calculation by current facts"
4.1 --- a/src/Pure/Isar/locale.ML Tue Apr 03 19:24:18 2007 +0200
4.2 +++ b/src/Pure/Isar/locale.ML Tue Apr 03 19:24:19 2007 +0200
4.3 @@ -160,7 +160,7 @@
4.4 (* For locales that define predicates this is [A [A]], where A is the locale
4.5 specification. Otherwise [].
4.6 Only required to generate the right witnesses for locales with predicates. *)
4.7 - import: expr, (*dynamic import*)
4.8 + imports: expr, (*dynamic imports*)
4.9 elems: (Element.context_i * stamp) list,
4.10 (* Static content, neither Fixes nor Constrains elements *)
4.11 params: ((string * typ) * mixfix) list, (*all params*)
4.12 @@ -286,10 +286,10 @@
4.13 val extend = I;
4.14
4.15 fun join_locales _
4.16 - ({axiom, import, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale,
4.17 + ({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale,
4.18 {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
4.19 {axiom = axiom,
4.20 - import = import,
4.21 + imports = imports,
4.22 elems = gen_merge_lists (eq_snd (op =)) elems elems',
4.23 params = params,
4.24 lparams = lparams,
4.25 @@ -349,12 +349,12 @@
4.26
4.27 fun change_locale name f thy =
4.28 let
4.29 - val {axiom, import, elems, params, lparams, decls, regs, intros} =
4.30 + val {axiom, imports, elems, params, lparams, decls, regs, intros} =
4.31 the_locale thy name;
4.32 - val (axiom', import', elems', params', lparams', decls', regs', intros') =
4.33 - f (axiom, import, elems, params, lparams, decls, regs, intros);
4.34 + val (axiom', imports', elems', params', lparams', decls', regs', intros') =
4.35 + f (axiom, imports, elems, params, lparams, decls, regs, intros);
4.36 in
4.37 - put_locale name {axiom = axiom', import = import', elems = elems',
4.38 + put_locale name {axiom = axiom', imports = imports', elems = elems',
4.39 params = params', lparams = lparams', decls = decls', regs = regs',
4.40 intros = intros'} thy
4.41 end;
4.42 @@ -421,8 +421,8 @@
4.43 gen_put_registration LocalLocalesData.map ProofContext.theory_of;
4.44
4.45 fun put_registration_in_locale name id =
4.46 - change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
4.47 - (axiom, import, elems, params, lparams, decls, regs @ [(id, [])], intros));
4.48 + change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
4.49 + (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros));
4.50
4.51
4.52 (* add witness theorem to registration in theory or context,
4.53 @@ -437,11 +437,11 @@
4.54 val add_local_witness = LocalLocalesData.map oo add_witness;
4.55
4.56 fun add_witness_in_locale name id thm =
4.57 - change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
4.58 + change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
4.59 let
4.60 fun add (id', thms) =
4.61 if id = id' then (id', thm :: thms) else (id', thms);
4.62 - in (axiom, import, elems, params, lparams, decls, map add regs, intros) end);
4.63 + in (axiom, imports, elems, params, lparams, decls, map add regs, intros) end);
4.64
4.65
4.66 (* printing of registrations *)
4.67 @@ -678,9 +678,9 @@
4.68
4.69 fun params_of (expr as Locale name) =
4.70 let
4.71 - val {import, params, ...} = the_locale thy name;
4.72 + val {imports, params, ...} = the_locale thy name;
4.73 val parms = map (fst o fst) params;
4.74 - val (parms', types', syn') = params_of import;
4.75 + val (parms', types', syn') = params_of imports;
4.76 val all_parms = merge_lists parms' parms;
4.77 val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
4.78 val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
4.79 @@ -818,9 +818,9 @@
4.80 identify at top level (top = true);
4.81 parms is accumulated list of parameters *)
4.82 let
4.83 - val {axiom, import, params, ...} = the_locale thy name;
4.84 + val {axiom, imports, params, ...} = the_locale thy name;
4.85 val ps = map (#1 o #1) params;
4.86 - val (ids', parms') = identify false import;
4.87 + val (ids', parms') = identify false imports;
4.88 (* acyclic import dependencies *)
4.89
4.90 val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
4.91 @@ -1381,24 +1381,24 @@
4.92 as a pair of singleton lists*)
4.93
4.94
4.95 -(* full context statements: import + elements + conclusion *)
4.96 +(* full context statements: imports + elements + conclusion *)
4.97
4.98 local
4.99
4.100 fun prep_context_statement prep_expr prep_elemss prep_facts
4.101 - do_close fixed_params import elements raw_concl context =
4.102 + do_close fixed_params imports elements raw_concl context =
4.103 let
4.104 val thy = ProofContext.theory_of context;
4.105
4.106 val (import_params, import_tenv, import_syn) =
4.107 - params_of_expr context fixed_params (prep_expr thy import)
4.108 + params_of_expr context fixed_params (prep_expr thy imports)
4.109 ([], Symtab.empty, Symtab.empty);
4.110 val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements;
4.111 val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params)
4.112 (map (prep_expr thy) includes) (import_params, import_tenv, import_syn);
4.113
4.114 val ((import_ids, _), raw_import_elemss) =
4.115 - flatten (context, prep_expr thy) (([], Symtab.empty), Expr import);
4.116 + flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports);
4.117 (* CB: normalise "includes" among elements *)
4.118 val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
4.119 ((import_ids, incl_syn), elements);
4.120 @@ -1441,19 +1441,19 @@
4.121 let
4.122 val thy = ProofContext.theory_of ctxt;
4.123 val locale = Option.map (prep_locale thy) raw_locale;
4.124 - val (fixed_params, import) =
4.125 + val (fixed_params, imports) =
4.126 (case locale of
4.127 NONE => ([], empty)
4.128 | SOME name =>
4.129 let val {params = ps, ...} = the_locale thy name
4.130 in (map fst ps, Locale name) end);
4.131 val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
4.132 - prep_ctxt false fixed_params import elems concl ctxt;
4.133 + prep_ctxt false fixed_params imports elems concl ctxt;
4.134 in (locale, locale_ctxt, elems_ctxt, concl') end;
4.135
4.136 -fun prep_expr prep import body ctxt =
4.137 +fun prep_expr prep imports body ctxt =
4.138 let
4.139 - val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt;
4.140 + val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt;
4.141 val all_elems = maps snd (import_elemss @ elemss);
4.142 in (all_elems, ctxt') end;
4.143
4.144 @@ -1462,8 +1462,8 @@
4.145 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
4.146 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
4.147
4.148 -fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt);
4.149 -fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
4.150 +fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt);
4.151 +fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt);
4.152
4.153 val read_expr = prep_expr read_context;
4.154 val cert_expr = prep_expr cert_context;
4.155 @@ -1484,8 +1484,8 @@
4.156
4.157 (* print locale *)
4.158
4.159 -fun print_locale thy show_facts import body =
4.160 - let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
4.161 +fun print_locale thy show_facts imports body =
4.162 + let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in
4.163 Pretty.big_list "locale elements:" (all_elems
4.164 |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
4.165 |> map (Element.pretty_ctxt ctxt) |> filter_out null
4.166 @@ -1576,8 +1576,8 @@
4.167 (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
4.168 val ctxt'' = ctxt' |> ProofContext.theory
4.169 (change_locale loc
4.170 - (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
4.171 - (axiom, import, elems @ [(Notes args', stamp ())],
4.172 + (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
4.173 + (axiom, imports, elems @ [(Notes args', stamp ())],
4.174 params, lparams, decls, regs, intros))
4.175 #> note_thmss_registrations loc args');
4.176 in ctxt'' end;
4.177 @@ -1592,8 +1592,8 @@
4.178
4.179 fun add_decls add loc decl =
4.180 ProofContext.theory (change_locale loc
4.181 - (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
4.182 - (axiom, import, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
4.183 + (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
4.184 + (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
4.185 add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
4.186
4.187 in
4.188 @@ -1783,7 +1783,7 @@
4.189 in fold_map change elemss defns end;
4.190
4.191 fun gen_add_locale prep_ctxt prep_expr
4.192 - predicate_name bname raw_import raw_body thy =
4.193 + predicate_name bname raw_imports raw_body thy =
4.194 (* predicate_name: NONE - open locale without predicate
4.195 SOME "" - locale with predicate named as locale
4.196 SOME "name" - locale with predicate named "name" *)
4.197 @@ -1795,10 +1795,10 @@
4.198 val thy_ctxt = ProofContext.init thy;
4.199 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
4.200 text as (parms, ((_, exts'), _), defs)) =
4.201 - prep_ctxt raw_import raw_body thy_ctxt;
4.202 + prep_ctxt raw_imports raw_body thy_ctxt;
4.203 val elemss = import_elemss @ body_elemss |>
4.204 map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
4.205 - val import = prep_expr thy raw_import;
4.206 + val imports = prep_expr thy raw_imports;
4.207
4.208 val extraTs = foldr Term.add_term_tfrees [] exts' \\
4.209 foldr Term.add_typ_tfrees [] (map snd parms);
4.210 @@ -1806,7 +1806,7 @@
4.211 else warning ("Additional type variable(s) in locale specification " ^ quote bname);
4.212
4.213 val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
4.214 - pred_thy), (import, regs)) =
4.215 + pred_thy), (imports, regs)) =
4.216 case predicate_name
4.217 of SOME predicate_name =>
4.218 let
4.219 @@ -1824,7 +1824,7 @@
4.220 val regs = mk_regs elemss''' axioms |>
4.221 map_filter (fn (("", _), _) => NONE | e => SOME e);
4.222 in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
4.223 - | NONE => ((((elemss, ([], []), []), ([], [])), thy), (import, []));
4.224 + | NONE => ((((elemss, ([], []), []), ([], [])), thy), (imports, []));
4.225
4.226 fun axiomify axioms elemss =
4.227 (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
4.228 @@ -1847,7 +1847,7 @@
4.229 |> declare_locale name
4.230 |> put_locale name
4.231 {axiom = axs',
4.232 - import = import,
4.233 + imports = imports,
4.234 elems = map (fn e => (e, stamp ())) elems'',
4.235 params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
4.236 lparams = map #1 (params_of' body_elemss),
5.1 --- a/src/Pure/Syntax/parser.ML Tue Apr 03 19:24:18 2007 +0200
5.2 +++ b/src/Pure/Syntax/parser.ML Tue Apr 03 19:24:19 2007 +0200
5.3 @@ -73,10 +73,10 @@
5.4 val chain_from = case (pri, rhs) of (~1, [Nonterminal (id, ~1)]) => SOME id | _ => NONE;
5.5
5.6 (*store chain if it does not already exist*)
5.7 - val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
5.8 - let val old_tos = these (AList.lookup (op =) chains from) in
5.9 + val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from_ =>
5.10 + let val old_tos = these (AList.lookup (op =) chains from_) in
5.11 if member (op =) old_tos lhs then (NONE, chains)
5.12 - else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains)
5.13 + else (SOME from_, AList.update (op =) (from_, insert (op =) lhs old_tos) chains)
5.14 end;
5.15
5.16 (*propagate new chain in lookahead and lambda lists;
5.17 @@ -411,7 +411,7 @@
5.18
5.19 fun pretty_nt (name, tag) =
5.20 let
5.21 - fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
5.22 + fun prod_of_chain from_ = ([Nonterminal (from_, ~1)], "", ~1);
5.23
5.24 val nt_prods =
5.25 Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @
5.26 @@ -553,8 +553,8 @@
5.27 val to_tag = convert_tag to;
5.28
5.29 fun make [] result = result
5.30 - | make (from :: froms) result = make froms ((to_tag,
5.31 - ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
5.32 + | make (from_ :: froms) result = make froms ((to_tag,
5.33 + ([Nonterminal (convert_tag from_, ~1)], "", ~1)) :: result);
5.34 in mk_chain_prods cs (make froms [] @ result) end;
5.35
5.36 val chain_prods = mk_chain_prods chains2 [];
6.1 --- a/src/Pure/Syntax/syn_ext.ML Tue Apr 03 19:24:18 2007 +0200
6.2 +++ b/src/Pure/Syntax/syn_ext.ML Tue Apr 03 19:24:19 2007 +0200
6.3 @@ -25,7 +25,7 @@
6.4 val logic: string
6.5 val args: string
6.6 val cargs: string
6.7 - val any: string
6.8 + val any_: string
6.9 val sprop: string
6.10 val typ_to_nonterm: typ -> string
6.11 datatype xsymb =
6.12 @@ -108,8 +108,8 @@
6.13 val sprop = "#prop";
6.14 val spropT = Type (sprop, []);
6.15
6.16 -val any = "any";
6.17 -val anyT = Type (any, []);
6.18 +val any_ = "any";
6.19 +val anyT = Type (any_, []);
6.20
6.21
6.22
6.23 @@ -181,7 +181,7 @@
6.24 | typ_to_nt default _ = default;
6.25
6.26 (*get nonterminal for rhs*)
6.27 -val typ_to_nonterm = typ_to_nt any;
6.28 +val typ_to_nonterm = typ_to_nt any_;
6.29
6.30 (*get nonterminal for lhs*)
6.31 val typ_to_nonterm1 = typ_to_nt logic;
7.1 --- a/src/Pure/Syntax/syntax.ML Tue Apr 03 19:24:18 2007 +0200
7.2 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 03 19:24:19 2007 +0200
7.3 @@ -313,7 +313,7 @@
7.4 val basic_nonterms =
7.5 (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
7.6 SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
7.7 - "asms", SynExt.any, SynExt.sprop, "num_const", "index", "struct"]);
7.8 + "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]);
7.9
7.10 val appl_syntax =
7.11 [("_appl", "[('b => 'a), args] => logic", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
8.1 --- a/src/Pure/thm.ML Tue Apr 03 19:24:18 2007 +0200
8.2 +++ b/src/Pure/thm.ML Tue Apr 03 19:24:19 2007 +0200
8.3 @@ -1577,13 +1577,13 @@
8.4 val lift = lift_rule (cprem_of state i);
8.5 val B = Logic.strip_assums_concl Bi;
8.6 val Hs = Logic.strip_assums_hyp Bi;
8.7 - val comp = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
8.8 + val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
8.9 fun res [] = Seq.empty
8.10 | res ((eres_flg, rule)::brules) =
8.11 if !Pattern.trace_unify_fail orelse
8.12 could_bires (Hs, B, eres_flg, rule)
8.13 then Seq.make (*delay processing remainder till needed*)
8.14 - (fn()=> SOME(comp (eres_flg, lift rule, nprems_of rule),
8.15 + (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule),
8.16 res brules))
8.17 else res brules
8.18 in Seq.flat (res brules) end;