tuned signature -- eliminated odd comment;
authorwenzelm
Wed Apr 27 20:58:40 2011 +0200 (2011-04-27)
changeset 42494eef1a23c9077
parent 42493 01430341fc79
child 42495 1af81b70cf09
tuned signature -- eliminated odd comment;
src/HOL/Tools/Quotient/quotient_def.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/variable.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Apr 27 20:37:56 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Wed Apr 27 20:58:40 2011 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5      fun sanity_test NONE _ = true
     1.6        | sanity_test (SOME bind) str =
     1.7 -          if Variable.name bind = str then true
     1.8 +          if Variable.check_name bind = str then true
     1.9            else error_msg bind str
    1.10  
    1.11      val _ = sanity_test optbind lhs_str
     2.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Apr 27 20:37:56 2011 +0200
     2.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Apr 27 20:58:40 2011 +0200
     2.3 @@ -254,7 +254,7 @@
     2.4          thy
     2.5          |> Sign.declare_const_global ((b, ty0), syn)
     2.6          |> snd
     2.7 -        |> pair ((Variable.name b, ty), (c, ty'))
     2.8 +        |> pair ((Variable.check_name b, ty), (c, ty'))
     2.9        end;
    2.10    in
    2.11      thy
     3.1 --- a/src/Pure/Isar/element.ML	Wed Apr 27 20:37:56 2011 +0200
     3.2 +++ b/src/Pure/Isar/element.ML	Wed Apr 27 20:58:40 2011 +0200
     3.3 @@ -99,7 +99,7 @@
     3.4  fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
     3.5    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
     3.6     | Constrains xs => Constrains (xs |> map (fn (x, T) =>
     3.7 -      (Variable.name (binding (Binding.name x)), typ T)))
     3.8 +      (Variable.check_name (binding (Binding.name x)), typ T)))
     3.9     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    3.10        ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    3.11     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    3.12 @@ -526,7 +526,7 @@
    3.13  
    3.14  fun activate raw_elem ctxt =
    3.15    let val elem = raw_elem |> map_ctxt
    3.16 -   {binding = tap Variable.name,
    3.17 +   {binding = tap Variable.check_name,
    3.18      typ = I,
    3.19      term = I,
    3.20      pattern = I,
     4.1 --- a/src/Pure/Isar/expression.ML	Wed Apr 27 20:37:56 2011 +0200
     4.2 +++ b/src/Pure/Isar/expression.ML	Wed Apr 27 20:58:40 2011 +0200
     4.3 @@ -128,7 +128,7 @@
     4.4      val (implicit, expr') = params_expr expr;
     4.5  
     4.6      val implicit' = map #1 implicit;
     4.7 -    val fixed' = map (Variable.name o #1) fixed;
     4.8 +    val fixed' = map (Variable.check_name o #1) fixed;
     4.9      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    4.10      val implicit'' =
    4.11        if strict then []
    4.12 @@ -393,7 +393,7 @@
    4.13      val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
    4.14  
    4.15      (* Retrieve parameter types *)
    4.16 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
    4.17 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
    4.18        | _ => fn ps => ps) (Fixes fors :: elems') [];
    4.19      val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
    4.20      val parms = xs ~~ Ts;  (* params from expression and elements *)
     5.1 --- a/src/Pure/Isar/local_defs.ML	Wed Apr 27 20:37:56 2011 +0200
     5.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Apr 27 20:58:40 2011 +0200
     5.3 @@ -92,7 +92,7 @@
     5.4    let
     5.5      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     5.6      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
     5.7 -    val xs = map Variable.name bvars;
     5.8 +    val xs = map Variable.check_name bvars;
     5.9      val names = map2 Thm.def_binding_optional bvars bfacts;
    5.10      val eqs = mk_def ctxt (xs ~~ rhss);
    5.11      val lhss = map (fst o Logic.dest_equals) eqs;
     6.1 --- a/src/Pure/Isar/obtain.ML	Wed Apr 27 20:37:56 2011 +0200
     6.2 +++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 20:58:40 2011 +0200
     6.3 @@ -119,7 +119,7 @@
     6.4      (*obtain vars*)
     6.5      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     6.6      val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
     6.7 -    val xs = map (Variable.name o #1) vars;
     6.8 +    val xs = map (Variable.check_name o #1) vars;
     6.9  
    6.10      (*obtain asms*)
    6.11      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    6.12 @@ -255,7 +255,7 @@
    6.13  
    6.14  fun inferred_type (binding, _, mx) ctxt =
    6.15    let
    6.16 -    val x = Variable.name binding;
    6.17 +    val x = Variable.check_name binding;
    6.18      val (T, ctxt') = Proof_Context.inferred_param x ctxt
    6.19    in ((x, T, mx), ctxt') end;
    6.20  
     7.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:37:56 2011 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:58:40 2011 +0200
     7.3 @@ -928,7 +928,7 @@
     7.4  fun prep_vars prep_typ internal =
     7.5    fold_map (fn (b, raw_T, mx) => fn ctxt =>
     7.6      let
     7.7 -      val x = Variable.name b;
     7.8 +      val x = Variable.check_name b;
     7.9        val _ = Lexicon.is_identifier (no_skolem internal x) orelse
    7.10          error ("Illegal variable name: " ^ Binding.print b);
    7.11  
     8.1 --- a/src/Pure/Isar/specification.ML	Wed Apr 27 20:37:56 2011 +0200
     8.2 +++ b/src/Pure/Isar/specification.ML	Wed Apr 27 20:58:40 2011 +0200
     8.3 @@ -169,7 +169,7 @@
     8.4  fun gen_axioms do_print prep raw_vars raw_specs thy =
     8.5    let
     8.6      val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
     8.7 -    val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
     8.8 +    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
     8.9  
    8.10      (*consts*)
    8.11      val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
    8.12 @@ -179,7 +179,7 @@
    8.13      val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
    8.14          fold_map Thm.add_axiom_global
    8.15            (map (apfst (fn a => Binding.map_name (K a) b))
    8.16 -            (Global_Theory.name_multi (Variable.name b) (map subst props)))
    8.17 +            (Global_Theory.name_multi (Variable.check_name b) (map subst props)))
    8.18          #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
    8.19  
    8.20      (*facts*)
    8.21 @@ -211,7 +211,7 @@
    8.22          [] => (Binding.name x, NoSyn)
    8.23        | [((b, _), mx)] =>
    8.24            let
    8.25 -            val y = Variable.name b;
    8.26 +            val y = Variable.check_name b;
    8.27              val _ = x = y orelse
    8.28                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
    8.29                  Position.str_of (Binding.pos_of b));
    8.30 @@ -250,7 +250,7 @@
    8.31          [] => (Binding.name x, NoSyn)
    8.32        | [((b, _), mx)] =>
    8.33            let
    8.34 -            val y = Variable.name b;
    8.35 +            val y = Variable.check_name b;
    8.36              val _ = x = y orelse
    8.37                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
    8.38                  Position.str_of (Binding.pos_of b));
    8.39 @@ -320,10 +320,10 @@
    8.40    | Element.Obtains obtains =>
    8.41        let
    8.42          val case_names = obtains |> map_index (fn (i, (b, _)) =>
    8.43 -          if Binding.is_empty b then string_of_int (i + 1) else Variable.name b);
    8.44 +          if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b);
    8.45          val constraints = obtains |> map (fn (_, (vars, _)) =>
    8.46            Element.Constrains
    8.47 -            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE)));
    8.48 +            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
    8.49  
    8.50          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    8.51          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
    8.52 @@ -333,7 +333,7 @@
    8.53          fun assume_case ((name, (vars, _)), asms) ctxt' =
    8.54            let
    8.55              val bs = map fst vars;
    8.56 -            val xs = map Variable.name bs;
    8.57 +            val xs = map Variable.check_name bs;
    8.58              val props = map fst asms;
    8.59              val (Ts, _) = ctxt'
    8.60                |> fold Variable.declare_term props
     9.1 --- a/src/Pure/variable.ML	Wed Apr 27 20:37:56 2011 +0200
     9.2 +++ b/src/Pure/variable.ML	Wed Apr 27 20:58:40 2011 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4    val sorts_of: Proof.context -> sort list
     9.5    val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
     9.6    val is_declared: Proof.context -> string -> bool
     9.7 -  val name: binding -> string
     9.8 +  val check_name: binding -> string
     9.9    val default_type: Proof.context -> string -> typ option
    9.10    val def_type: Proof.context -> bool -> indexname -> typ option
    9.11    val def_sort: Proof.context -> indexname -> sort option
    9.12 @@ -164,8 +164,7 @@
    9.13  
    9.14  val is_declared = Name.is_declared o names_of;
    9.15  
    9.16 -(*checked name binding*)
    9.17 -val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
    9.18 +val check_name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
    9.19  
    9.20  
    9.21  
    9.22 @@ -362,7 +361,7 @@
    9.23          [] => ()
    9.24        | dups => err_dups dups);
    9.25  
    9.26 -    val xs = map name bs;
    9.27 +    val xs = map check_name bs;
    9.28      val names = names_of ctxt;
    9.29      val (xs', names') =
    9.30        if is_body ctxt then Name.variants xs names |>> map Name.skolem