# HG changeset patch # User wenzelm # Date 1175621059 -7200 # Node ID 2ac646ab2f6c9770fc4d8ce18be13eb58b4d8d6d # Parent c6bbe56afbf797d33cde59780709ded650f09a49 avoid clash with Alice keywords; diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Isar/calculation.ML Tue Apr 03 19:24:19 2007 +0200 @@ -16,7 +16,8 @@ val symmetric: attribute val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq - val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq + val finally_: (thmref * Attrib.src list) list option -> bool -> + Proof.state -> Proof.state Seq.seq val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq val moreover: bool -> Proof.state -> Proof.state val ultimately: bool -> Proof.state -> Proof.state @@ -154,7 +155,7 @@ val also = calculate Proof.get_thmss false; val also_i = calculate (K I) false; -val finally = calculate Proof.get_thmss true; +val finally_ = calculate Proof.get_thmss true; val finally_i = calculate (K I) true; diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Apr 03 19:24:19 2007 +0200 @@ -459,9 +459,9 @@ val print_locales = Toplevel.unknown_theory o Toplevel.keep (Locale.print_locales o Toplevel.theory_of); -fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o +fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o Toplevel.keep (fn state => - Locale.print_locale (Toplevel.theory_of state) show_facts import body); + Locale.print_locale (Toplevel.theory_of state) show_facts imports body); fun print_registrations show_wits name = Toplevel.unknown_context o Toplevel.keep (Toplevel.node_case diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Apr 03 19:24:19 2007 +0200 @@ -665,7 +665,7 @@ val finallyP = OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" (K.tag_proof K.prf_chain) - (calc_args >> (Toplevel.proofs' o Calculation.finally)); + (calc_args >> (Toplevel.proofs' o Calculation.finally_)); val moreoverP = OuterSyntax.command "moreover" "augment calculation by current facts" diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Isar/locale.ML Tue Apr 03 19:24:19 2007 +0200 @@ -160,7 +160,7 @@ (* For locales that define predicates this is [A [A]], where A is the locale specification. Otherwise []. Only required to generate the right witnesses for locales with predicates. *) - import: expr, (*dynamic import*) + imports: expr, (*dynamic imports*) elems: (Element.context_i * stamp) list, (* Static content, neither Fixes nor Constrains elements *) params: ((string * typ) * mixfix) list, (*all params*) @@ -286,10 +286,10 @@ val extend = I; fun join_locales _ - ({axiom, import, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale, + ({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale, {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) = {axiom = axiom, - import = import, + imports = imports, elems = gen_merge_lists (eq_snd (op =)) elems elems', params = params, lparams = lparams, @@ -349,12 +349,12 @@ fun change_locale name f thy = let - val {axiom, import, elems, params, lparams, decls, regs, intros} = + val {axiom, imports, elems, params, lparams, decls, regs, intros} = the_locale thy name; - val (axiom', import', elems', params', lparams', decls', regs', intros') = - f (axiom, import, elems, params, lparams, decls, regs, intros); + val (axiom', imports', elems', params', lparams', decls', regs', intros') = + f (axiom, imports, elems, params, lparams, decls, regs, intros); in - put_locale name {axiom = axiom', import = import', elems = elems', + put_locale name {axiom = axiom', imports = imports', elems = elems', params = params', lparams = lparams', decls = decls', regs = regs', intros = intros'} thy end; @@ -421,8 +421,8 @@ gen_put_registration LocalLocalesData.map ProofContext.theory_of; fun put_registration_in_locale name id = - change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) => - (axiom, import, elems, params, lparams, decls, regs @ [(id, [])], intros)); + change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) => + (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros)); (* add witness theorem to registration in theory or context, @@ -437,11 +437,11 @@ val add_local_witness = LocalLocalesData.map oo add_witness; fun add_witness_in_locale name id thm = - change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) => + change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) => let fun add (id', thms) = if id = id' then (id', thm :: thms) else (id', thms); - in (axiom, import, elems, params, lparams, decls, map add regs, intros) end); + in (axiom, imports, elems, params, lparams, decls, map add regs, intros) end); (* printing of registrations *) @@ -678,9 +678,9 @@ fun params_of (expr as Locale name) = let - val {import, params, ...} = the_locale thy name; + val {imports, params, ...} = the_locale thy name; val parms = map (fst o fst) params; - val (parms', types', syn') = params_of import; + val (parms', types', syn') = params_of imports; val all_parms = merge_lists parms' parms; val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make); val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make); @@ -818,9 +818,9 @@ identify at top level (top = true); parms is accumulated list of parameters *) let - val {axiom, import, params, ...} = the_locale thy name; + val {axiom, imports, params, ...} = the_locale thy name; val ps = map (#1 o #1) params; - val (ids', parms') = identify false import; + val (ids', parms') = identify false imports; (* acyclic import dependencies *) val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids'); @@ -1381,24 +1381,24 @@ as a pair of singleton lists*) -(* full context statements: import + elements + conclusion *) +(* full context statements: imports + elements + conclusion *) local fun prep_context_statement prep_expr prep_elemss prep_facts - do_close fixed_params import elements raw_concl context = + do_close fixed_params imports elements raw_concl context = let val thy = ProofContext.theory_of context; val (import_params, import_tenv, import_syn) = - params_of_expr context fixed_params (prep_expr thy import) + params_of_expr context fixed_params (prep_expr thy imports) ([], Symtab.empty, Symtab.empty); val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements; val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params) (map (prep_expr thy) includes) (import_params, import_tenv, import_syn); val ((import_ids, _), raw_import_elemss) = - flatten (context, prep_expr thy) (([], Symtab.empty), Expr import); + flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports); (* CB: normalise "includes" among elements *) val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy)) ((import_ids, incl_syn), elements); @@ -1441,19 +1441,19 @@ let val thy = ProofContext.theory_of ctxt; val locale = Option.map (prep_locale thy) raw_locale; - val (fixed_params, import) = + val (fixed_params, imports) = (case locale of NONE => ([], empty) | SOME name => let val {params = ps, ...} = the_locale thy name in (map fst ps, Locale name) end); val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') = - prep_ctxt false fixed_params import elems concl ctxt; + prep_ctxt false fixed_params imports elems concl ctxt; in (locale, locale_ctxt, elems_ctxt, concl') end; -fun prep_expr prep import body ctxt = +fun prep_expr prep imports body ctxt = let - val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt; + val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt; val all_elems = maps snd (import_elemss @ elemss); in (all_elems, ctxt') end; @@ -1462,8 +1462,8 @@ val read_ctxt = prep_context_statement intern_expr read_elemss read_facts; val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts; -fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt); -fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt); +fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt); +fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt); val read_expr = prep_expr read_context; val cert_expr = prep_expr cert_context; @@ -1484,8 +1484,8 @@ (* print locale *) -fun print_locale thy show_facts import body = - let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in +fun print_locale thy show_facts imports body = + let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in Pretty.big_list "locale elements:" (all_elems |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) |> map (Element.pretty_ctxt ctxt) |> filter_out null @@ -1576,8 +1576,8 @@ (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]); val ctxt'' = ctxt' |> ProofContext.theory (change_locale loc - (fn (axiom, import, elems, params, lparams, decls, regs, intros) => - (axiom, import, elems @ [(Notes args', stamp ())], + (fn (axiom, imports, elems, params, lparams, decls, regs, intros) => + (axiom, imports, elems @ [(Notes args', stamp ())], params, lparams, decls, regs, intros)) #> note_thmss_registrations loc args'); in ctxt'' end; @@ -1592,8 +1592,8 @@ fun add_decls add loc decl = ProofContext.theory (change_locale loc - (fn (axiom, import, elems, params, lparams, decls, regs, intros) => - (axiom, import, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #> + (fn (axiom, imports, elems, params, lparams, decls, regs, intros) => + (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #> add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])]; in @@ -1783,7 +1783,7 @@ in fold_map change elemss defns end; fun gen_add_locale prep_ctxt prep_expr - predicate_name bname raw_import raw_body thy = + predicate_name bname raw_imports raw_body thy = (* predicate_name: NONE - open locale without predicate SOME "" - locale with predicate named as locale SOME "name" - locale with predicate named "name" *) @@ -1795,10 +1795,10 @@ val thy_ctxt = ProofContext.init thy; val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), text as (parms, ((_, exts'), _), defs)) = - prep_ctxt raw_import raw_body thy_ctxt; + prep_ctxt raw_imports raw_body thy_ctxt; val elemss = import_elemss @ body_elemss |> map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE); - val import = prep_expr thy raw_import; + val imports = prep_expr thy raw_imports; val extraTs = foldr Term.add_term_tfrees [] exts' \\ foldr Term.add_typ_tfrees [] (map snd parms); @@ -1806,7 +1806,7 @@ else warning ("Additional type variable(s) in locale specification " ^ quote bname); val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros), - pred_thy), (import, regs)) = + pred_thy), (imports, regs)) = case predicate_name of SOME predicate_name => let @@ -1824,7 +1824,7 @@ val regs = mk_regs elemss''' axioms |> map_filter (fn (("", _), _) => NONE | e => SOME e); in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end - | NONE => ((((elemss, ([], []), []), ([], [])), thy), (import, [])); + | NONE => ((((elemss, ([], []), []), ([], [])), thy), (imports, [])); fun axiomify axioms elemss = (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let @@ -1847,7 +1847,7 @@ |> declare_locale name |> put_locale name {axiom = axs', - import = import, + imports = imports, elems = map (fn e => (e, stamp ())) elems'', params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), lparams = map #1 (params_of' body_elemss), diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Syntax/parser.ML Tue Apr 03 19:24:19 2007 +0200 @@ -73,10 +73,10 @@ val chain_from = case (pri, rhs) of (~1, [Nonterminal (id, ~1)]) => SOME id | _ => NONE; (*store chain if it does not already exist*) - val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from => - let val old_tos = these (AList.lookup (op =) chains from) in + val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from_ => + let val old_tos = these (AList.lookup (op =) chains from_) in if member (op =) old_tos lhs then (NONE, chains) - else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains) + else (SOME from_, AList.update (op =) (from_, insert (op =) lhs old_tos) chains) end; (*propagate new chain in lookahead and lambda lists; @@ -411,7 +411,7 @@ fun pretty_nt (name, tag) = let - fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); + fun prod_of_chain from_ = ([Nonterminal (from_, ~1)], "", ~1); val nt_prods = Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @ @@ -553,8 +553,8 @@ val to_tag = convert_tag to; fun make [] result = result - | make (from :: froms) result = make froms ((to_tag, - ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result); + | make (from_ :: froms) result = make froms ((to_tag, + ([Nonterminal (convert_tag from_, ~1)], "", ~1)) :: result); in mk_chain_prods cs (make froms [] @ result) end; val chain_prods = mk_chain_prods chains2 []; diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Tue Apr 03 19:24:19 2007 +0200 @@ -25,7 +25,7 @@ val logic: string val args: string val cargs: string - val any: string + val any_: string val sprop: string val typ_to_nonterm: typ -> string datatype xsymb = @@ -108,8 +108,8 @@ val sprop = "#prop"; val spropT = Type (sprop, []); -val any = "any"; -val anyT = Type (any, []); +val any_ = "any"; +val anyT = Type (any_, []); @@ -181,7 +181,7 @@ | typ_to_nt default _ = default; (*get nonterminal for rhs*) -val typ_to_nonterm = typ_to_nt any; +val typ_to_nonterm = typ_to_nt any_; (*get nonterminal for lhs*) val typ_to_nonterm1 = typ_to_nt logic; diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 03 19:24:19 2007 +0200 @@ -313,7 +313,7 @@ val basic_nonterms = (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes", SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", - "asms", SynExt.any, SynExt.sprop, "num_const", "index", "struct"]); + "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]); val appl_syntax = [("_appl", "[('b => 'a), args] => logic", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)), diff -r c6bbe56afbf7 -r 2ac646ab2f6c src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Apr 03 19:24:18 2007 +0200 +++ b/src/Pure/thm.ML Tue Apr 03 19:24:19 2007 +0200 @@ -1577,13 +1577,13 @@ val lift = lift_rule (cprem_of state i); val B = Logic.strip_assums_concl Bi; val Hs = Logic.strip_assums_hyp Bi; - val comp = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true); + val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true); fun res [] = Seq.empty | res ((eres_flg, rule)::brules) = if !Pattern.trace_unify_fail orelse could_bires (Hs, B, eres_flg, rule) then Seq.make (*delay processing remainder till needed*) - (fn()=> SOME(comp (eres_flg, lift rule, nprems_of rule), + (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule), res brules)) else res brules in Seq.flat (res brules) end;