--- 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