avoid clash with Alice keywords;
authorwenzelm
Tue Apr 03 19:24:19 2007 +0200 (2007-04-03 ago)
changeset 225732ac646ab2f6c
parent 22572 c6bbe56afbf7
child 22574 e6c25fd3de2a
avoid clash with Alice keywords;
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/thm.ML
     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;