--- a/src/HOL/Tools/Quotient/quotient_def.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed Apr 27 20:58:40 2011 +0200
@@ -51,7 +51,7 @@
fun sanity_test NONE _ = true
| sanity_test (SOME bind) str =
- if Variable.name bind = str then true
+ if Variable.check_name bind = str then true
else error_msg bind str
val _ = sanity_test optbind lhs_str
--- a/src/Pure/Isar/class_declaration.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML Wed Apr 27 20:58:40 2011 +0200
@@ -254,7 +254,7 @@
thy
|> Sign.declare_const_global ((b, ty0), syn)
|> snd
- |> pair ((Variable.name b, ty), (c, ty'))
+ |> pair ((Variable.check_name b, ty), (c, ty'))
end;
in
thy
--- a/src/Pure/Isar/element.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/element.ML Wed Apr 27 20:58:40 2011 +0200
@@ -99,7 +99,7 @@
fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
- (Variable.name (binding (Binding.name x)), typ T)))
+ (Variable.check_name (binding (Binding.name x)), typ T)))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -526,7 +526,7 @@
fun activate raw_elem ctxt =
let val elem = raw_elem |> map_ctxt
- {binding = tap Variable.name,
+ {binding = tap Variable.check_name,
typ = I,
term = I,
pattern = I,
--- a/src/Pure/Isar/expression.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/expression.ML Wed Apr 27 20:58:40 2011 +0200
@@ -128,7 +128,7 @@
val (implicit, expr') = params_expr expr;
val implicit' = map #1 implicit;
- val fixed' = map (Variable.name o #1) fixed;
+ val fixed' = map (Variable.check_name o #1) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
val implicit'' =
if strict then []
@@ -393,7 +393,7 @@
val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
- val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.name o #1) fixes)
+ val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Variable.check_name o #1) fixes)
| _ => fn ps => ps) (Fixes fors :: elems') [];
val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)
--- a/src/Pure/Isar/local_defs.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML Wed Apr 27 20:58:40 2011 +0200
@@ -92,7 +92,7 @@
let
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
- val xs = map Variable.name bvars;
+ val xs = map Variable.check_name bvars;
val names = map2 Thm.def_binding_optional bvars bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
--- a/src/Pure/Isar/obtain.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Apr 27 20:58:40 2011 +0200
@@ -119,7 +119,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
- val xs = map (Variable.name o #1) vars;
+ val xs = map (Variable.check_name o #1) vars;
(*obtain asms*)
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -255,7 +255,7 @@
fun inferred_type (binding, _, mx) ctxt =
let
- val x = Variable.name binding;
+ val x = Variable.check_name binding;
val (T, ctxt') = Proof_Context.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
--- a/src/Pure/Isar/proof_context.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 27 20:58:40 2011 +0200
@@ -928,7 +928,7 @@
fun prep_vars prep_typ internal =
fold_map (fn (b, raw_T, mx) => fn ctxt =>
let
- val x = Variable.name b;
+ val x = Variable.check_name b;
val _ = Lexicon.is_identifier (no_skolem internal x) orelse
error ("Illegal variable name: " ^ Binding.print b);
--- a/src/Pure/Isar/specification.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/Isar/specification.ML Wed Apr 27 20:58:40 2011 +0200
@@ -169,7 +169,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
- val xs = map (fn ((b, T), _) => (Variable.name b, T)) vars;
+ val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
(*consts*)
val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
@@ -179,7 +179,7 @@
val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
fold_map Thm.add_axiom_global
(map (apfst (fn a => Binding.map_name (K a) b))
- (Global_Theory.name_multi (Variable.name b) (map subst props)))
+ (Global_Theory.name_multi (Variable.check_name b) (map subst props)))
#>> (fn ths => ((b, atts), [(map #2 ths, [])])));
(*facts*)
@@ -211,7 +211,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Variable.name b;
+ val y = Variable.check_name b;
val _ = x = y orelse
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -250,7 +250,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Variable.name b;
+ val y = Variable.check_name b;
val _ = x = y orelse
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -320,10 +320,10 @@
| Element.Obtains obtains =>
let
val case_names = obtains |> map_index (fn (i, (b, _)) =>
- if Binding.is_empty b then string_of_int (i + 1) else Variable.name b);
+ if Binding.is_empty b then string_of_int (i + 1) else Variable.check_name b);
val constraints = obtains |> map (fn (_, (vars, _)) =>
Element.Constrains
- (vars |> map_filter (fn (x, SOME T) => SOME (Variable.name x, T) | _ => NONE)));
+ (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -333,7 +333,7 @@
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
val bs = map fst vars;
- val xs = map Variable.name bs;
+ val xs = map Variable.check_name bs;
val props = map fst asms;
val (Ts, _) = ctxt'
|> fold Variable.declare_term props
--- a/src/Pure/variable.ML Wed Apr 27 20:37:56 2011 +0200
+++ b/src/Pure/variable.ML Wed Apr 27 20:58:40 2011 +0200
@@ -15,7 +15,7 @@
val sorts_of: Proof.context -> sort list
val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
val is_declared: Proof.context -> string -> bool
- val name: binding -> string
+ val check_name: binding -> string
val default_type: Proof.context -> string -> typ option
val def_type: Proof.context -> bool -> indexname -> typ option
val def_sort: Proof.context -> indexname -> sort option
@@ -164,8 +164,7 @@
val is_declared = Name.is_declared o names_of;
-(*checked name binding*)
-val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
+val check_name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
@@ -362,7 +361,7 @@
[] => ()
| dups => err_dups dups);
- val xs = map name bs;
+ val xs = map check_name bs;
val names = names_of ctxt;
val (xs', names') =
if is_body ctxt then Name.variants xs names |>> map Name.skolem