merged.
--- a/NEWS Thu Dec 04 08:47:45 2008 -0800
+++ b/NEWS Thu Dec 04 09:12:41 2008 -0800
@@ -55,9 +55,24 @@
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML
interface instead.
+* There is a new lexical item "float" with syntax ["-"] digit+ "." digit+,
+without spaces.
+
*** Pure ***
+* Type Binding.T gradually replaces formerly used type bstring for names
+to be bound. Name space interface for declarations has been simplified:
+
+ NameSpace.declare: NameSpace.naming
+ -> Binding.T -> NameSpace.T -> string * NameSpace.T
+ NameSpace.bind: NameSpace.naming
+ -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
+ (*exception Symtab.DUP*)
+
+See further modules src/Pure/General/binding.ML and
+src/Pure/General/name_space.ML
+
* Module moves in repository:
src/Pure/Tools/value.ML ~> src/Tools/
src/Pure/Tools/quickcheck.ML ~> src/Tools/
@@ -269,6 +284,9 @@
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY.
+* The real numbers offer decimal input syntax: 12.34 is translated into
+ 1234/10^4. This translation is not reversed upon output.
+
* New ML antiquotation @{code}: takes constant as argument, generates
corresponding code in background and inserts name of the corresponding
resulting ML value/function/datatype constructor binding in place.
--- a/src/HOL/Code_Eval.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Code_Eval.thy Thu Dec 04 09:12:41 2008 -0800
@@ -63,7 +63,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))
+ |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit_global
--- a/src/HOL/Import/hol4rews.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Import/hol4rews.ML Thu Dec 04 09:12:41 2008 -0800
@@ -282,7 +282,7 @@
val thy = case opt_get_output_thy thy of
"" => thy
| output_thy => if internal
- then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+ then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
else thy
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
val curmaps = HOL4ConstMaps.get thy
@@ -324,7 +324,7 @@
val thy = case opt_get_output_thy thy of
"" => thy
| output_thy => if internal
- then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+ then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
else thy
val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
val curmaps = HOL4ConstMaps.get thy
@@ -348,7 +348,7 @@
fun add_hol4_pending bthy bthm hth thy =
let
- val thmname = Sign.full_name thy bthm
+ val thmname = Sign.full_bname thy bthm
val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
val curpend = HOL4Pending.get thy
val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
--- a/src/HOL/Import/proof_kernel.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Import/proof_kernel.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1960,7 +1960,7 @@
val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
SOME (_,res) => HOLThm(rens_of linfo,res)
| NONE => raise ERR "new_definition" "Bad conclusion"
- val fullname = Sign.full_name thy22 thmname
+ val fullname = Sign.full_bname thy22 thmname
val thy22' = case opt_get_output_thy thy22 of
"" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
add_hol4_mapping thyname thmname fullname thy22)
--- a/src/HOL/List.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/List.thy Thu Dec 04 09:12:41 2008 -0800
@@ -3423,7 +3423,7 @@
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
nibbles nibbles;
in
- PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
+ PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
end
*}
--- a/src/HOL/Nominal/Nominal.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Nominal/Nominal.thy Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
theory Nominal
imports Main Infinite_Set
uses
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Dec 04 09:12:41 2008 -0800
@@ -170,7 +170,7 @@
val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy =>
let
val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
- val swap_name = Sign.full_name thy ("swap_" ^ ak_name);
+ val swap_name = Sign.full_bname thy ("swap_" ^ ak_name);
val a = Free ("a", T);
val b = Free ("b", T);
val c = Free ("c", T);
@@ -199,10 +199,10 @@
val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy =>
let
val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
- val swap_name = Sign.full_name thy ("swap_" ^ ak_name)
+ val swap_name = Sign.full_bname thy ("swap_" ^ ak_name)
val prmT = mk_permT T --> T --> T;
val prm_name = ak_name ^ "_prm_" ^ ak_name;
- val qu_prm_name = Sign.full_name thy prm_name;
+ val qu_prm_name = Sign.full_bname thy prm_name;
val x = Free ("x", HOLogic.mk_prodT (T, T));
val xs = Free ("xs", mk_permT T);
val a = Free ("a", T) ;
@@ -235,7 +235,7 @@
val pi = Free ("pi", mk_permT T);
val a = Free ("a", T');
val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
- val cperm_def = Const (Sign.full_name thy' perm_def_name, mk_permT T --> T' --> T');
+ val cperm_def = Const (Sign.full_bname thy' perm_def_name, mk_permT T --> T' --> T');
val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
val def = Logic.mk_equals
@@ -250,7 +250,7 @@
val (prm_cons_thms,thy6) =
thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
let
- val ak_name_qu = Sign.full_name thy5 (ak_name);
+ val ak_name_qu = Sign.full_bname thy5 (ak_name);
val i_type = Type(ak_name_qu,[]);
val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
val at_type = Logic.mk_type i_type;
@@ -299,9 +299,9 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
AxClass.define_class (cl_name, ["HOL.type"]) []
- [((Name.binding (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
- ((Name.binding (cl_name ^ "2"), []), [axiom2]),
- ((Name.binding (cl_name ^ "3"), []), [axiom3])] thy
+ [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
+ ((Binding.name (cl_name ^ "2"), []), [axiom2]),
+ ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
end) ak_names_types thy6;
(* proves that every pt_<ak>-type together with <ak>-type *)
@@ -311,8 +311,8 @@
val (prm_inst_thms,thy8) =
thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
let
- val ak_name_qu = Sign.full_name thy7 ak_name;
- val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name);
+ val ak_name_qu = Sign.full_bname thy7 ak_name;
+ val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
val i_type1 = TFree("'x",[pt_name_qu]);
val i_type2 = Type(ak_name_qu,[]);
val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
@@ -338,7 +338,7 @@
val (fs_ax_classes,thy11) = fold_map (fn (ak_name, T) => fn thy =>
let
val cl_name = "fs_"^ak_name;
- val pt_name = Sign.full_name thy ("pt_"^ak_name);
+ val pt_name = Sign.full_bname thy ("pt_"^ak_name);
val ty = TFree("'a",["HOL.type"]);
val x = Free ("x", ty);
val csupp = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
@@ -347,7 +347,7 @@
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
in
- AxClass.define_class (cl_name, [pt_name]) [] [((Name.binding (cl_name ^ "1"), []), [axiom1])] thy
+ AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
end) ak_names_types thy8;
(* proves that every fs_<ak>-type together with <ak>-type *)
@@ -357,8 +357,8 @@
val (fs_inst_thms,thy12) =
thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
let
- val ak_name_qu = Sign.full_name thy11 ak_name;
- val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name);
+ val ak_name_qu = Sign.full_bname thy11 ak_name;
+ val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
val i_type1 = TFree("'x",[fs_name_qu]);
val i_type2 = Type(ak_name_qu,[]);
val cfs = Const ("Nominal.fs",
@@ -397,7 +397,7 @@
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
AxClass.define_class (cl_name, ["HOL.type"]) []
- [((Name.binding (cl_name ^ "1"), []), [ax1])] thy'
+ [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
(* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem; *)
@@ -406,9 +406,9 @@
val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy =>
fold_map (fn (ak_name', T') => fn thy' =>
let
- val ak_name_qu = Sign.full_name thy' (ak_name);
- val ak_name_qu' = Sign.full_name thy' (ak_name');
- val cp_name_qu = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
+ val ak_name_qu = Sign.full_bname thy' (ak_name);
+ val ak_name_qu' = Sign.full_bname thy' (ak_name');
+ val cp_name_qu = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name');
val i_type0 = TFree("'a",[cp_name_qu]);
val i_type1 = Type(ak_name_qu,[]);
val i_type2 = Type(ak_name_qu',[]);
@@ -442,8 +442,8 @@
(if not (ak_name = ak_name')
then
let
- val ak_name_qu = Sign.full_name thy' ak_name;
- val ak_name_qu' = Sign.full_name thy' ak_name';
+ val ak_name_qu = Sign.full_bname thy' ak_name;
+ val ak_name_qu' = Sign.full_bname thy' ak_name';
val i_type1 = Type(ak_name_qu,[]);
val i_type2 = Type(ak_name_qu',[]);
val cdj = Const ("Nominal.disjoint",
@@ -487,8 +487,8 @@
val thy13 = fold (fn ak_name => fn thy =>
fold (fn ak_name' => fn thy' =>
let
- val qu_name = Sign.full_name thy' ak_name';
- val cls_name = Sign.full_name thy' ("pt_"^ak_name);
+ val qu_name = Sign.full_bname thy' ak_name';
+ val cls_name = Sign.full_bname thy' ("pt_"^ak_name);
val at_inst = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
val proof1 = EVERY [Class.intro_classes_tac [],
@@ -518,7 +518,7 @@
(* are instances of pt_<ak> *)
val thy18 = fold (fn ak_name => fn thy =>
let
- val cls_name = Sign.full_name thy ("pt_"^ak_name);
+ val cls_name = Sign.full_bname thy ("pt_"^ak_name);
val at_thm = PureThy.get_thm thy ("at_"^ak_name^"_inst");
val pt_inst = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
@@ -562,8 +562,8 @@
val thy20 = fold (fn ak_name => fn thy =>
fold (fn ak_name' => fn thy' =>
let
- val qu_name = Sign.full_name thy' ak_name';
- val qu_class = Sign.full_name thy' ("fs_"^ak_name);
+ val qu_name = Sign.full_bname thy' ak_name';
+ val qu_class = Sign.full_bname thy' ("fs_"^ak_name);
val proof =
(if ak_name = ak_name'
then
@@ -588,7 +588,7 @@
val thy24 = fold (fn ak_name => fn thy =>
let
- val cls_name = Sign.full_name thy ("fs_"^ak_name);
+ val cls_name = Sign.full_bname thy ("fs_"^ak_name);
val fs_inst = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
@@ -628,8 +628,8 @@
fold (fn ak_name' => fn thy' =>
fold (fn ak_name'' => fn thy'' =>
let
- val name = Sign.full_name thy'' ak_name;
- val cls_name = Sign.full_name thy'' ("cp_"^ak_name'^"_"^ak_name'');
+ val name = Sign.full_bname thy'' ak_name;
+ val cls_name = Sign.full_bname thy'' ("cp_"^ak_name'^"_"^ak_name'');
val proof =
(if (ak_name'=ak_name'') then
(let
@@ -666,7 +666,7 @@
val thy26 = fold (fn ak_name => fn thy =>
fold (fn ak_name' => fn thy' =>
let
- val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
+ val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name');
val cp_inst = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
val pt_inst = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
val at_inst = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
@@ -698,7 +698,7 @@
fun discrete_pt_inst discrete_ty defn =
fold (fn ak_name => fn thy =>
let
- val qu_class = Sign.full_name thy ("pt_"^ak_name);
+ val qu_class = Sign.full_bname thy ("pt_"^ak_name);
val simp_s = HOL_basic_ss addsimps [defn];
val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
in
@@ -708,7 +708,7 @@
fun discrete_fs_inst discrete_ty defn =
fold (fn ak_name => fn thy =>
let
- val qu_class = Sign.full_name thy ("fs_"^ak_name);
+ val qu_class = Sign.full_bname thy ("fs_"^ak_name);
val supp_def = @{thm "Nominal.supp_def"};
val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
@@ -719,7 +719,7 @@
fun discrete_cp_inst discrete_ty defn =
fold (fn ak_name' => (fold (fn ak_name => fn thy =>
let
- val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
+ val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
val supp_def = @{thm "Nominal.supp_def"};
val simp_s = HOL_ss addsimps [defn];
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
--- a/src/HOL/Nominal/nominal_induct.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Nominal/nominal_induct.ML Thu Dec 04 09:12:41 2008 -0800
@@ -6,7 +6,7 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> (Name.binding option * term) option list list ->
+ val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
thm list -> int -> RuleCases.cases_tactic
val nominal_induct_method: Method.src -> Proof.context -> Method.method
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Dec 04 09:12:41 2008 -0800
@@ -182,7 +182,7 @@
fun mk_avoids params name sets =
let
val (_, ctxt') = ProofContext.add_fixes_i
- (map (fn (s, T) => (Name.binding s, SOME T, NoSyn)) params) ctxt;
+ (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
fun mk s =
let
val t = Syntax.read_term ctxt' s;
--- a/src/HOL/Nominal/nominal_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Nominal/nominal_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -227,7 +227,7 @@
map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
val ps = map (fn (_, n, _, _) =>
- (Sign.full_name tmp_thy n, Sign.full_name tmp_thy (n ^ "_Rep"))) dts;
+ (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
val rps = map Library.swap ps;
fun replace_types (Type ("Nominal.ABS", [T, U])) =
@@ -241,7 +241,7 @@
map replace_types cargs, NoSyn)) constrs)) dts';
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val full_new_type_names' = map (Sign.full_name thy) new_type_names';
+ val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
val ({induction, ...},thy1) =
DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
@@ -263,7 +263,7 @@
val perm_names' = DatatypeProp.indexify_names (map (fn (i, _) =>
"perm_" ^ name_of_typ (nth_dtyp i)) descr);
val perm_names = replicate (length new_type_names) "Nominal.perm" @
- map (Sign.full_name thy1) (List.drop (perm_names', length new_type_names));
+ map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
val perm_names_types = perm_names ~~ perm_types;
val perm_names_types' = perm_names' ~~ perm_types;
@@ -289,7 +289,7 @@
else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
end;
in
- (Attrib.no_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
(Free (nth perm_names_types' i) $
Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
list_comb (c, args),
@@ -301,7 +301,7 @@
PrimrecPackage.add_primrec_overloaded
(map (fn (s, sT) => (s, sT, false))
(List.take (perm_names' ~~ perm_names_types, length new_type_names)))
- (map (fn s => (Name.binding s, NONE, NoSyn)) perm_names') perm_eqs thy1;
+ (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
(**** prove that permutation functions introduced by unfolding are ****)
(**** equivalent to already existing permutation functions ****)
@@ -566,16 +566,16 @@
(rep_set_name, T))
end)
(descr ~~ rep_set_names))));
- val rep_set_names'' = map (Sign.full_name thy3) rep_set_names';
+ val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
- alt_name = Name.binding big_rep_name, coind = false, no_elim = true, no_ind = false,
+ alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true}
- (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
+ (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
- [] (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy3;
+ [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
(**** Prove that representing set is closed under permutation ****)
@@ -768,7 +768,7 @@
val newTs' = Library.take (length new_type_names, recTs');
val newTs = Library.take (length new_type_names, recTs);
- val full_new_type_names = map (Sign.full_name thy) new_type_names;
+ val full_new_type_names = map (Sign.full_bname thy) new_type_names;
fun make_constr_def tname T T' ((thy, defs, eqns),
(((cname_rep, _), (cname, cargs)), (cname', mx))) =
@@ -1432,7 +1432,7 @@
if length descr'' = 1 then [big_rec_name] else
map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr''));
- val rec_set_names = map (Sign.full_name thy10) rec_set_names';
+ val rec_set_names = map (Sign.full_bname thy10) rec_set_names';
val rec_fns = map (uncurry (mk_Free "f"))
(rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
@@ -1509,12 +1509,12 @@
thy10 |>
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = Name.binding big_rec_name, coind = false, no_elim = false, no_ind = false,
+ alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true}
- (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] ||>
- PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
+ (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
+ PureThy.hide_fact true (NameSpace.append (Sign.full_bname thy10 big_rec_name) "induct");
(** equivariance **)
@@ -2002,7 +2002,7 @@
(* define primrec combinators *)
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
- val reccomb_names = map (Sign.full_name thy11)
+ val reccomb_names = map (Sign.full_bname thy11)
(if length descr'' = 1 then [big_reccomb_name] else
(map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
(1 upto (length descr''))));
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Dec 04 09:12:41 2008 -0800
@@ -9,13 +9,13 @@
signature NOMINAL_PRIMREC =
sig
val add_primrec: string -> string list option -> string option ->
- ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
+ ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_unchecked: string -> string list option -> string option ->
- ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
+ ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_i: string -> term list option -> term option ->
- ((Name.binding * term) * attribute list) list -> theory -> Proof.state
+ ((Binding.T * term) * attribute list) list -> theory -> Proof.state
val add_primrec_unchecked_i: string -> term list option -> term option ->
- ((Name.binding * term) * attribute list) list -> theory -> Proof.state
+ ((Binding.T * term) * attribute list) list -> theory -> Proof.state
end;
structure NominalPrimrec : NOMINAL_PRIMREC =
--- a/src/HOL/Statespace/state_space.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Statespace/state_space.ML Thu Dec 04 09:12:41 2008 -0800
@@ -268,7 +268,7 @@
(map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var")
,[SOME (n,NONE)])) all_comps);
- val full_name = Sign.full_name thy name;
+ val full_name = Sign.full_bname thy name;
val dist_thm_name = distinct_compsN;
val dist_thm_full_name =
let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps "";
@@ -302,7 +302,7 @@
val attr = Attrib.internal type_attr;
- val assumes = Element.Assumes [((Name.binding dist_thm_name,[attr]),
+ val assumes = Element.Assumes [((Binding.name dist_thm_name,[attr]),
[(HOLogic.Trueprop $
(Const ("DistinctTreeProver.all_distinct",
Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
@@ -373,7 +373,7 @@
fun statespace_definition state_type args name parents parent_comps components thy =
let
- val full_name = Sign.full_name thy name;
+ val full_name = Sign.full_bname thy name;
val all_comps = parent_comps @ components;
val components' = map (fn (n,T) => (n,(T,full_name))) components;
@@ -443,7 +443,7 @@
NONE => []
| SOME s =>
let
- val fx = Element.Fixes [(Name.binding s,SOME (string_of_typ stateT),NoSyn)];
+ val fx = Element.Fixes [(Binding.name s,SOME (string_of_typ stateT),NoSyn)];
val cs = Element.Constrains
(map (fn (n,T) => (n,string_of_typ T))
((map (fn (n,_) => (n,nameT)) all_comps) @
@@ -490,7 +490,7 @@
fun add_parent (Ts,pname,rs) env =
let
- val full_pname = Sign.full_name thy pname;
+ val full_pname = Sign.full_bname thy pname;
val {args,components,...} =
(case get_statespace (Context.Theory thy) full_pname of
SOME r => r
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Dec 04 09:12:41 2008 -0800
@@ -108,7 +108,7 @@
if length descr' = 1 then [big_rec_name'] else
map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
(1 upto (length descr'));
- val rec_set_names = map (Sign.full_name thy0) rec_set_names';
+ val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
@@ -156,11 +156,11 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = Name.binding big_rec_name', coind = false, no_elim = false, no_ind = true,
+ alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true}
- (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
+ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] thy0;
+ (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
(* prove uniqueness and termination of primrec combinators *)
@@ -226,7 +226,7 @@
(* define primrec combinators *)
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
- val reccomb_names = map (Sign.full_name thy1)
+ val reccomb_names = map (Sign.full_bname thy1)
(if length descr' = 1 then [big_reccomb_name] else
(map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -294,7 +294,7 @@
in Const (@{const_name undefined}, Ts @ Ts' ---> T')
end) constrs) descr';
- val case_names = map (fn s => Sign.full_name thy1 (s ^ "_case")) new_type_names;
+ val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
(* define case combinators via primrec combinators *)
@@ -317,7 +317,7 @@
val fns = (List.concat (Library.take (i, case_dummy_fns))) @
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
- val decl = ((Name.binding (Sign.base_name name), caseT), NoSyn);
+ val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
val def = ((Sign.base_name name) ^ "_def",
Logic.mk_equals (list_comb (Const (name, caseT), fns1),
list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
--- a/src/HOL/Tools/datatype_codegen.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Dec 04 09:12:41 2008 -0800
@@ -440,7 +440,7 @@
(mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
- (NONE, (Attrib.no_binding, def')) lthy;
+ (NONE, (Attrib.empty_binding, def')) lthy;
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
--- a/src/HOL/Tools/datatype_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/datatype_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -567,7 +567,7 @@
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
- let val full_tname = Sign.full_name tmp_thy (Syntax.type_name tname mx)
+ let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
in (case duplicates (op =) tvs of
[] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
@@ -586,8 +586,8 @@
val _ = (case fold (curry add_typ_tfree_names) cargs' [] \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
- Sign.full_name_path tmp_thy tname) (Syntax.const_name cname mx'),
+ in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
+ Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg =>
@@ -600,7 +600,7 @@
in
case duplicates (op =) (map fst constrs') of
[] =>
- (dts' @ [(i, (Sign.full_name tmp_thy (Syntax.type_name tname mx),
+ (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
map DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
| dups => error ("Duplicate constructors " ^ commas dups ^
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 04 09:12:41 2008 -0800
@@ -77,7 +77,7 @@
(if length descr' = 1 then [big_rec_name] else
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
- val rep_set_names = map (Sign.full_name thy1) rep_set_names';
+ val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
val leafTs' = get_nonrec_types descr' sorts;
@@ -184,10 +184,10 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
InductivePackage.add_inductive_global (serial_string ())
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
- alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
+ alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true}
- (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
- (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy1;
+ (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
+ (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
(********************************* typedef ********************************)
@@ -210,7 +210,7 @@
val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
(1 upto (length (flat (tl descr))));
val all_rep_names = map (Sign.intern_const thy3) rep_names @
- map (Sign.full_name thy3) rep_names';
+ map (Sign.full_bname thy3) rep_names';
(* isomorphism declarations *)
--- a/src/HOL/Tools/function_package/fundef_common.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/fundef_common.ML Thu Dec 04 09:12:41 2008 -0800
@@ -82,7 +82,7 @@
psimps, pinducts, termination, defname}) phi =
let
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
- val name = Name.name_of o Morphism.name phi o Name.binding
+ val name = Name.name_of o Morphism.binding phi o Binding.name
in
FundefCtxData { add_simps = add_simps, case_names = case_names,
fs = map term fs, R = term R, psimps = fact psimps,
--- a/src/HOL/Tools/function_package/fundef_core.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/fundef_core.ML Thu Dec 04 09:12:41 2008 -0800
@@ -485,7 +485,7 @@
|> Syntax.check_term lthy
val ((f, (_, f_defthm)), lthy) =
- LocalTheory.define Thm.internalK ((Name.binding (function_name fname), mixfix), ((Name.binding fdefname, []), f_def)) lthy
+ LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
in
((f, f_defthm), lthy)
end
@@ -898,7 +898,7 @@
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
val (_, lthy) =
- LocalTheory.abbrev Syntax.mode_default ((Name.binding (dom_name defname), NoSyn), mk_acc domT R) lthy
+ LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
val newthy = ProofContext.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
--- a/src/HOL/Tools/function_package/fundef_lib.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Thu Dec 04 09:12:41 2008 -0800
@@ -56,7 +56,7 @@
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
let
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
- val (_, ctx') = ProofContext.add_fixes_i [(Name.binding n', SOME T, NoSyn)] ctx
+ val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
val (n'', body) = Term.dest_abs (n', T, b)
val _ = (n' = n'') orelse error "dest_all_ctx"
--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -9,14 +9,14 @@
signature FUNDEF_PACKAGE =
sig
- val add_fundef : (Name.binding * string option * mixfix) list
+ val add_fundef : (Binding.T * string option * mixfix) list
-> (Attrib.binding * string) list
-> FundefCommon.fundef_config
-> bool list
-> local_theory
-> Proof.state
- val add_fundef_i: (Name.binding * typ option * mixfix) list
+ val add_fundef_i: (Binding.T * typ option * mixfix) list
-> (Attrib.binding * term) list
-> FundefCommon.fundef_config
-> bool list
@@ -36,7 +36,7 @@
open FundefLib
open FundefCommon
-fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Name.binding name, atts), ths)
+fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Binding.name name, atts), ths)
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
@@ -147,10 +147,10 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
in
lthy
- |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.rule_del]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
|> ProofContext.note_thmss_i ""
- [((Name.binding "termination", [ContextRules.intro_bang (SOME 0)]),
+ [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
|> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
end
--- a/src/HOL/Tools/function_package/inductive_wrap.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML Thu Dec 04 09:12:41 2008 -0800
@@ -44,14 +44,14 @@
{quiet_mode = false,
verbose = ! Toplevel.debug,
kind = Thm.internalK,
- alt_name = Name.no_binding,
+ alt_name = Binding.empty,
coind = false,
no_elim = false,
no_ind = false,
skip_mono = true}
- [((Name.binding R, T), NoSyn)] (* the relation *)
+ [((Binding.name R, T), NoSyn)] (* the relation *)
[] (* no parameters *)
- (map (fn t => (Attrib.no_binding, t)) defs) (* the intros *)
+ (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
[] (* no special monos *)
lthy
--- a/src/HOL/Tools/function_package/mutual.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/mutual.ML Thu Dec 04 09:12:41 2008 -0800
@@ -150,8 +150,8 @@
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
let
val ((f, (_, f_defthm)), lthy') =
- LocalTheory.define Thm.internalK ((Name.binding fname, mixfix),
- ((Name.binding (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
+ LocalTheory.define Thm.internalK ((Binding.name fname, mixfix),
+ ((Binding.name (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
--- a/src/HOL/Tools/function_package/size.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/function_package/size.ML Thu Dec 04 09:12:41 2008 -0800
@@ -89,7 +89,7 @@
map (fn (T as Type (s, _), optname) =>
let
val s' = the_default (Sign.base_name s) optname ^ "_size";
- val s'' = Sign.full_name thy s'
+ val s'' = Sign.full_bname thy s'
in
(s'',
(list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
@@ -133,7 +133,7 @@
let
val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
- ((Name.binding c, NoSyn), ((Name.binding def_name, []), rhs));
+ ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
in (thm', lthy') end;
--- a/src/HOL/Tools/inductive_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/inductive_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/inductive_package.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
@@ -39,17 +38,17 @@
thm list list * local_theory
type inductive_flags
val add_inductive_i:
- inductive_flags -> ((Name.binding * typ) * mixfix) list ->
+ inductive_flags -> ((Binding.T * typ) * mixfix) list ->
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
inductive_result * local_theory
val add_inductive: bool -> bool ->
- (Name.binding * string option * mixfix) list ->
- (Name.binding * string option * mixfix) list ->
+ (Binding.T * string option * mixfix) list ->
+ (Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list ->
(Facts.ref * Attrib.src list) list ->
local_theory -> inductive_result * local_theory
val add_inductive_global: string -> inductive_flags ->
- ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+ ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> theory -> inductive_result * theory
val arities_of: thm -> (string * int) list
val params_of: thm -> term list
@@ -64,16 +63,16 @@
sig
include BASIC_INDUCTIVE_PACKAGE
type add_ind_def
- val declare_rules: string -> Name.binding -> bool -> bool -> string list ->
- thm list -> Name.binding list -> Attrib.src list list -> (thm * string list) list ->
+ val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
+ thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
thm -> local_theory -> thm list * thm list * thm * local_theory
val add_ind_def: add_ind_def
val gen_add_inductive_i: add_ind_def -> inductive_flags ->
- ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+ ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
thm list -> local_theory -> inductive_result * local_theory
val gen_add_inductive: add_ind_def -> bool -> bool ->
- (Name.binding * string option * mixfix) list ->
- (Name.binding * string option * mixfix) list ->
+ (Binding.T * string option * mixfix) list ->
+ (Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> inductive_result * local_theory
val gen_ind_decl: add_ind_def -> bool ->
@@ -638,14 +637,14 @@
(* add definiton of recursive predicates to theory *)
val rec_name =
- if Binding.is_nothing alt_name then
- Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ if Binding.is_empty alt_name then
+ Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
else alt_name;
val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
LocalTheory.define Thm.internalK
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
- (Attrib.no_binding, fold_rev lambda params
+ (Attrib.empty_binding, fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
(cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
@@ -656,7 +655,7 @@
val xs = map Free (Variable.variant_frees ctxt intr_ts
(mk_names "x" (length Ts) ~~ Ts))
in
- (name_mx, (Attrib.no_binding, fold_rev lambda (params @ xs)
+ (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
(list_comb (rec_const, params @ make_bool_args' bs i @
make_args argTs (xs ~~ Ts)))))
end) (cnames_syn ~~ cs);
@@ -673,7 +672,7 @@
elims raw_induct ctxt =
let
val rec_name = Name.name_of rec_binding;
- val rec_qualified = Name.qualified rec_name;
+ val rec_qualified = Binding.qualify rec_name;
val intr_names = map Name.name_of intr_bindings;
val ind_case_names = RuleCases.case_names intr_names;
val induct =
@@ -693,23 +692,23 @@
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
ctxt1 |>
- LocalTheory.note kind ((rec_qualified (Name.binding "intros"), []), intrs') ||>>
+ LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
fold_map (fn (name, (elim, cases)) =>
- LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
+ LocalTheory.note kind ((Binding.name (NameSpace.qualified (Sign.base_name name) "cases"),
[Attrib.internal (K (RuleCases.case_names cases)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.cases_pred name)),
Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
LocalTheory.note kind
- ((rec_qualified (Name.binding (coind_prefix coind ^ "induct")),
+ ((rec_qualified (Binding.name (coind_prefix coind ^ "induct")),
map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
val ctxt3 = if no_ind orelse coind then ctxt2 else
let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
in
ctxt2 |>
- LocalTheory.notes kind [((rec_qualified (Name.binding "inducts"), []),
+ LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
inducts |> map (fn (name, th) => ([th],
[Attrib.internal (K ind_case_names),
Attrib.internal (K (RuleCases.consumes 1)),
@@ -718,13 +717,13 @@
in (intrs', elims', induct', ctxt3) end;
type inductive_flags =
- {quiet_mode: bool, verbose: bool, kind: string, alt_name: Name.binding,
+ {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
type add_ind_def =
inductive_flags ->
term list -> (Attrib.binding * term) list -> thm list ->
- term list -> (Name.binding * mixfix) list ->
+ term list -> (Binding.T * mixfix) list ->
local_theory -> inductive_result * local_theory
fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
@@ -735,7 +734,7 @@
val _ = message (quiet_mode andalso not verbose)
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
- val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn; (* FIXME *)
+ val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn; (* FIXME *)
val ((intr_names, intr_atts), intr_ts) =
apfst split_list (split_list (map (check_rule ctxt cs params) intros));
@@ -846,7 +845,7 @@
val intrs = map (apsnd the_single) specs;
val monos = Attrib.eval_thms lthy raw_monos;
val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
- alt_name = Name.no_binding, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
+ alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
in
lthy
|> LocalTheory.set_group (serial_string ())
@@ -858,7 +857,7 @@
fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
let
- val name = Sign.full_name thy (Name.name_of (fst (fst (hd cnames_syn))));
+ val name = Sign.full_bname thy (Name.name_of (fst (fst (hd cnames_syn))));
val ctxt' = thy
|> TheoryTarget.init NONE
|> LocalTheory.set_group group
--- a/src/HOL/Tools/inductive_realizer.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Dec 04 09:12:41 2008 -0800
@@ -338,7 +338,7 @@
(Logic.strip_assums_concl rintr));
val s' = Sign.base_name s;
val T' = Logic.unvarifyT T
- in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
+ in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
(List.take (snd (strip_comb
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
@@ -347,10 +347,10 @@
val (ind_info, thy3') = thy2 |>
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
+ {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
- ((Name.binding (Sign.base_name (name_of_thm intr)), []),
+ ((Binding.name (Sign.base_name (name_of_thm intr)), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
(rintrs ~~ maps snd rss)) [] ||>
Sign.absolute_path;
--- a/src/HOL/Tools/inductive_set_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/inductive_set_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/inductive_set_package.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Wrapper for defining inductive sets using package for inductive predicates,
@@ -13,13 +12,13 @@
val pred_set_conv_att: attribute
val add_inductive_i:
InductivePackage.inductive_flags ->
- ((Name.binding * typ) * mixfix) list ->
+ ((Binding.T * typ) * mixfix) list ->
(string * typ) list ->
(Attrib.binding * term) list -> thm list ->
local_theory -> InductivePackage.inductive_result * local_theory
val add_inductive: bool -> bool ->
- (Name.binding * string option * mixfix) list ->
- (Name.binding * string option * mixfix) list ->
+ (Binding.T * string option * mixfix) list ->
+ (Binding.T * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
local_theory -> InductivePackage.inductive_result * local_theory
val codegen_preproc: theory -> thm list -> thm list
@@ -464,17 +463,17 @@
| NONE => u)) |>
Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
- val cnames_syn' = map (fn (b, _) => (Name.map_name (suffix "p") b, NoSyn)) cnames_syn;
+ val cnames_syn' = map (fn (b, _) => (Binding.map_base (suffix "p") b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
InductivePackage.add_ind_def
- {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Name.no_binding,
+ {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
cs' intros' monos' params1 cnames_syn' ctxt;
(* define inductive sets using previously defined predicates *)
val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
- (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.no_binding,
+ (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
fold_rev lambda params (HOLogic.Collect_const U $
HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds)) ctxt1;
@@ -492,17 +491,17 @@
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, split_conv]) 1))
in
- ctxt |> LocalTheory.note kind ((Name.binding (s ^ "p_" ^ s ^ "_eq"),
+ ctxt |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
[Attrib.internal (K pred_set_conv_att)]),
[conv_thm]) |> snd
end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
(* convert theorems to set notation *)
val rec_name =
- if Binding.is_nothing alt_name then
- Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ if Binding.is_empty alt_name then
+ Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
else alt_name;
- val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *)
+ val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
val (intrs', elims', induct, ctxt4) =
--- a/src/HOL/Tools/primrec_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/primrec_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/primrec_package.ML
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen; Norbert Voelker, FernUni Hagen;
Florian Haftmann, TU Muenchen
@@ -8,12 +7,12 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: (Name.binding * typ option * mixfix) list ->
+ val add_primrec: (Binding.T * typ option * mixfix) list ->
(Attrib.binding * term) list -> local_theory -> thm list * local_theory
- val add_primrec_global: (Name.binding * typ option * mixfix) list ->
+ val add_primrec_global: (Binding.T * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
- (Name.binding * typ option * mixfix) list ->
+ (Binding.T * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
end;
@@ -196,7 +195,7 @@
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
- in (var, ((Name.binding def_name, []), rhs)) end;
+ in (var, ((Binding.name def_name, []), rhs)) end;
(* find datatypes which contain all datatypes in tnames' *)
@@ -248,7 +247,7 @@
val _ = if gen_eq_set (op =) (names1, names2) then ()
else primrec_error ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
- val qualify = Name.qualified
+ val qualify = Binding.qualify
(space_implode "_" (map (Sign.base_name o #1) defs));
val spec' = (map o apfst o apfst) qualify spec;
val simp_atts = map (Attrib.internal o K)
@@ -260,7 +259,7 @@
|-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
|-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
|-> (fn simps' => LocalTheory.note Thm.theoremK
- ((qualify (Name.binding "simps"), simp_atts), maps snd simps'))
+ ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
|>> snd
end handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
--- a/src/HOL/Tools/recdef_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/recdef_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -268,8 +268,8 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
- [] (Element.Shows [(Attrib.no_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+ Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
+ [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
--- a/src/HOL/Tools/record_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/record_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1762,8 +1762,8 @@
val external_names = NameSpace.external_names (Sign.naming_of thy);
val alphas = map fst args;
- val name = Sign.full_name thy bname;
- val full = Sign.full_name_path thy bname;
+ val name = Sign.full_bname thy bname;
+ val full = Sign.full_bname_path thy bname;
val base = Sign.base_name;
val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
@@ -2253,7 +2253,7 @@
(* errors *)
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
val err_dup_record =
if is_none (get_record thy name) then []
else ["Duplicate definition of record " ^ quote name];
--- a/src/HOL/Tools/res_axioms.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/res_axioms.ML Thu Dec 04 09:12:41 2008 -0800
@@ -84,10 +84,10 @@
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
(*Forms a lambda-abstraction over the formal parameters*)
val (c, thy') =
- Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy
+ Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
val cdef = cname ^ "_def"
val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
- val ax = Thm.axiom thy'' (Sign.full_name thy'' cdef)
+ val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
| dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
(*Universal quant: insert a free variable into body and continue*)
--- a/src/HOL/Tools/typecopy_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/typecopy_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -143,7 +143,7 @@
|> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
|> `(fn lthy => Syntax.check_term lthy def_eq)
|-> (fn def_eq => Specification.definition
- (NONE, (Attrib.no_binding, def_eq)))
+ (NONE, (Attrib.empty_binding, def_eq)))
|-> (fn (_, (_, def_thm)) =>
Class.prove_instantiation_exit_result Morphism.thm
(fn _ => fn def_thm => Class.intro_classes_tac []
--- a/src/HOL/Tools/typedef_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Tools/typedef_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -80,7 +80,7 @@
let
val _ = Theory.requires thy "Typedef" "typedefs";
val ctxt = ProofContext.init thy;
- val full = Sign.full_name thy;
+ val full = Sign.full_bname thy;
(*rhs*)
val full_name = full name;
--- a/src/HOL/Typedef.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Typedef.thy Thu Dec 04 09:12:41 2008 -0800
@@ -145,7 +145,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
+ |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit_global
--- a/src/HOL/Typerep.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/Typerep.thy Thu Dec 04 09:12:41 2008 -0800
@@ -67,7 +67,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
+ |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit_global
--- a/src/HOL/ex/Quickcheck.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/ex/Quickcheck.thy Thu Dec 04 09:12:41 2008 -0800
@@ -151,11 +151,11 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort random})
|> PrimrecPackage.add_primrec
- [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
- (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
+ [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
+ (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
|-> add_code
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
+ |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit_global
--- a/src/HOL/ex/Term_Of_Syntax.thy Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOL/ex/Term_Of_Syntax.thy Thu Dec 04 09:12:41 2008 -0800
@@ -10,7 +10,7 @@
begin
setup {*
- Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
+ Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
#> snd
*}
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu Dec 04 09:12:41 2008 -0800
@@ -120,7 +120,7 @@
in (* local *)
fun add_axioms (comp_dnam, eqs : eq list) thy' = let
- val comp_dname = Sign.full_name thy' comp_dnam;
+ val comp_dname = Sign.full_bname thy' comp_dnam;
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
fun copy_app dname = %%:(dname^"_copy")`Bound 0;
--- a/src/HOLCF/Tools/domain/domain_extender.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Thu Dec 04 09:12:41 2008 -0800
@@ -100,7 +100,7 @@
fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
let
val dtnvs = map ((fn (dname,vs) =>
- (Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
+ (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
o fst) eqs''';
val cons''' = map snd eqs''';
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Dec 04 09:12:41 2008 -0800
@@ -607,7 +607,7 @@
val dnames = map (fst o fst) eqs;
val conss = map snd eqs;
-val comp_dname = Sign.full_name thy comp_dnam;
+val comp_dname = Sign.full_bname thy comp_dnam;
val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
val pg = pg' thy;
--- a/src/HOLCF/Tools/fixrec_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOLCF/Tools/fixrec_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: HOLCF/Tools/fixrec_package.ML
- ID: $Id$
Author: Amber Telfer and Brian Huffman
Recursive function definition package for HOLCF.
@@ -10,9 +9,9 @@
val legacy_infer_term: theory -> term -> term
val legacy_infer_prop: theory -> term -> term
val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
- val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
+ val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory
val add_fixpat: Attrib.binding * string list -> theory -> theory
- val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
+ val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory
end;
structure FixrecPackage: FIXREC_PACKAGE =
--- a/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -54,7 +54,7 @@
fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
let
val ctxt = ProofContext.init thy;
- val full = Sign.full_name thy;
+ val full = Sign.full_bname thy;
(*rhs*)
val full_name = full name;
@@ -94,7 +94,7 @@
|> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
val less_def' = Syntax.check_term lthy3 less_def;
val ((_, (_, less_definition')), lthy4) = lthy3
- |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), less_def'));
+ |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
val thy5 = lthy4
--- a/src/Pure/General/binding.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/General/binding.ML Thu Dec 04 09:12:41 2008 -0800
@@ -15,17 +15,16 @@
sig
include BASIC_BINDING
type T
- val binding_pos: string * Position.T -> T
- val binding: string -> T
- val no_binding: T
- val dest_binding: T -> (string * bool) list * string
- val is_nothing: T -> bool
- val pos_of: T -> Position.T
-
- val map_binding: ((string * bool) list * string -> (string * bool) list * string)
- -> T -> T
+ val name_pos: string * Position.T -> T
+ val name: string -> T
+ val empty: T
+ val map_base: (string -> string) -> T -> T
+ val qualify: string -> T -> T
val add_prefix: bool -> string -> T -> T
val map_prefix: ((string * bool) list -> T -> T) -> T -> T
+ val is_empty: T -> bool
+ val pos_of: T -> Position.T
+ val dest: T -> (string * bool) list * string
val display: T -> string
end
@@ -44,22 +43,30 @@
datatype T = Binding of ((string * bool) list * string) * Position.T;
(* (prefix components (with mandatory flag), base name, position) *)
-fun binding_pos (name, pos) = Binding (([], name), pos);
-fun binding name = binding_pos (name, Position.none);
-val no_binding = binding "";
-
-fun pos_of (Binding (_, pos)) = pos;
-fun dest_binding (Binding (prefix_name, _)) = prefix_name;
+fun name_pos (name, pos) = Binding (([], name), pos);
+fun name name = name_pos (name, Position.none);
+val empty = name "";
fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
-fun is_nothing (Binding ((_, name), _)) = name = "";
+val map_base = map_binding o apsnd;
+
+fun qualify_base path name =
+ if path = "" orelse name = "" then name
+ else path ^ "." ^ name;
+
+val qualify = map_base o qualify_base;
+ (*FIXME should all operations on bare names moved here from name_space.ML ?*)
fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
else (map_binding o apfst) (cons (prfx, sticky)) b;
fun map_prefix f (Binding ((prefix, name), pos)) =
- f prefix (binding_pos (name, pos));
+ f prefix (name_pos (name, pos));
+
+fun is_empty (Binding ((_, name), _)) = name = "";
+fun pos_of (Binding (_, pos)) = pos;
+fun dest (Binding (prefix_name, _)) = prefix_name;
fun display (Binding ((prefix, name), _)) =
let
--- a/src/Pure/General/name_space.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/General/name_space.ML Thu Dec 04 09:12:41 2008 -0800
@@ -30,27 +30,24 @@
val get_accesses: T -> string -> xstring list
val merge: T * T -> T
type naming
- val path_of: naming -> string
+ val default_naming: naming
+ val declare: naming -> Binding.T -> T -> string * T
+ val full_name: naming -> Binding.T -> string
+ val declare_base: naming -> string -> T -> T
val external_names: naming -> string -> string list
- val full: naming -> bstring -> string
- val declare: naming -> string -> T -> T
- val default_naming: naming
+ val path_of: naming -> string
val add_path: string -> naming -> naming
val no_base_names: naming -> naming
val qualified_names: naming -> naming
val sticky_prefix: string -> naming -> naming
- val full_binding: naming -> Binding.T -> string
- val declare_binding: naming -> Binding.T -> T -> string * T
type 'a table = T * 'a Symtab.table
val empty_table: 'a table
- val table_declare: naming -> Binding.T * 'a
+ val bind: naming -> Binding.T * 'a
-> 'a table -> string * 'a table (*exception Symtab.DUP*)
- val table_declare_permissive: naming -> Binding.T * 'a
- -> 'a table -> string * 'a table
- val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
val dest_table: 'a table -> (string * 'a) list
val extern_table: 'a table -> (xstring * 'a) list
+ val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
end;
structure NameSpace: NAME_SPACE =
@@ -269,7 +266,11 @@
fun full (Naming (path, (qualify, _))) = qualify path;
-fun declare naming name space =
+fun full_name naming b =
+ let val (prefix, bname) = Binding.dest b
+ in full (apply_prefix prefix naming) bname end;
+
+fun declare_base naming name space =
if is_hidden name then
error ("Attempt to declare hidden name " ^ quote name)
else
@@ -281,12 +282,12 @@
val (accs, accs') = pairself (map implode_name) (accesses naming names);
in space |> fold (add_name name) accs |> put_accesses name accs' end;
-fun declare_binding bnaming b =
+fun declare bnaming b =
let
- val (prefix, bname) = Binding.dest_binding b;
+ val (prefix, bname) = Binding.dest b;
val naming = apply_prefix prefix bnaming;
val name = full naming bname;
- in declare naming name #> pair name end;
+ in declare_base naming name #> pair name end;
@@ -296,21 +297,14 @@
val empty_table = (empty, Symtab.empty);
-fun gen_table_declare update naming (binding, x) (space, tab) =
+fun bind naming (b, x) (space, tab) =
let
- val (name, space') = declare_binding naming binding space;
- in (name, (space', update (name, x) tab)) end;
-
-fun table_declare naming = gen_table_declare Symtab.update_new naming;
-fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
-
-fun full_binding naming b =
- let val (prefix, bname) = Binding.dest_binding b
- in full (apply_prefix prefix naming) bname end;
+ val (name, space') = declare naming b space;
+ in (name, (space', Symtab.update_new (name, x) tab)) end;
fun extend_table naming bentries (space, tab) =
let val entries = map (apfst (full naming)) bentries
- in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
+ in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
(merge (space1, space2), Symtab.merge eq (tab1, tab2));
--- a/src/Pure/Isar/args.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/args.ML Thu Dec 04 09:12:41 2008 -0800
@@ -35,7 +35,7 @@
val name_source: T list -> string * T list
val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
val name: T list -> string * T list
- val binding: T list -> Name.binding * T list
+ val binding: T list -> Binding.T * T list
val alt_name: T list -> string * T list
val symbol: T list -> string * T list
val liberal_name: T list -> string * T list
@@ -66,8 +66,8 @@
val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
val attribs: (string -> string) -> T list -> src list * T list
val opt_attribs: (string -> string) -> T list -> src list * T list
- val thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
- val opt_thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
+ val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
+ val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
src -> Proof.context -> 'a * Proof.context
@@ -171,7 +171,7 @@
val name_source_position = named >> T.source_position_of;
val name = named >> T.content_of;
-val binding = P.position name >> Binding.binding_pos;
+val binding = P.position name >> Binding.name_pos;
val alt_name = alt_string >> T.content_of;
val symbol = symbolic >> T.content_of;
val liberal_name = symbol || name;
@@ -280,8 +280,8 @@
fun opt_thm_name intern s =
Scan.optional
- ((binding -- opt_attribs intern || attribs intern >> pair Name.no_binding) --| $$$ s)
- (Name.no_binding, []);
+ ((binding -- opt_attribs intern || attribs intern >> pair Binding.empty) --| $$$ s)
+ (Binding.empty, []);
--- a/src/Pure/Isar/attrib.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/attrib.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/attrib.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Symbolic representation of attributes -- with name and syntax.
@@ -8,8 +7,8 @@
signature ATTRIB =
sig
type src = Args.src
- type binding = Name.binding * src list
- val no_binding: binding
+ type binding = Binding.T * src list
+ val empty_binding: binding
val print_attributes: theory -> unit
val intern: theory -> xstring -> string
val intern_src: theory -> src -> src
@@ -55,8 +54,8 @@
type src = Args.src;
-type binding = Name.binding * src list;
-val no_binding: binding = (Name.no_binding, []);
+type binding = Binding.T * src list;
+val empty_binding: binding = (Binding.empty, []);
@@ -119,7 +118,7 @@
fun attribute thy = attribute_i thy o intern_src thy;
fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
- [((Name.no_binding, []),
+ [((Binding.empty, []),
map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
|> fst |> maps snd;
@@ -373,7 +372,7 @@
fun register_config config thy =
let
val bname = Config.name_of config;
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
in
thy
|> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
--- a/src/Pure/Isar/calculation.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/calculation.ML Thu Dec 04 09:12:41 2008 -0800
@@ -115,7 +115,7 @@
fun print_calculation false _ _ = ()
| print_calculation true ctxt calc = Pretty.writeln
- (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt calculationN, calc));
+ (ProofContext.pretty_fact ctxt (ProofContext.full_bname ctxt calculationN, calc));
(* also and finally *)
--- a/src/Pure/Isar/class.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/class.ML Thu Dec 04 09:12:41 2008 -0800
@@ -96,7 +96,7 @@
thy
|> fold2 add_constraint (map snd consts) no_constraints
|> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
- (map SOME inst, map (pair (Attrib.no_binding) o Thm.prop_of) def_facts)
+ (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
||> fold2 add_constraint (map snd consts) constraints
end;
@@ -476,7 +476,7 @@
val inst = the_inst thy' class;
val params = map (apsnd fst o snd) (these_params thy' [class]);
- val c' = Sign.full_name thy' c;
+ val c' = Sign.full_bname thy' c;
val dict' = Morphism.term phi dict;
val dict_def = map_types Logic.unvarifyT dict';
val ty' = Term.fastype_of dict_def;
@@ -485,7 +485,7 @@
fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
in
thy'
- |> Sign.declare_const pos ((Name.binding c, ty''), mx) |> snd
+ |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
|> Thm.add_def false false (c, def_eq)
|>> Thm.symmetric
||>> get_axiom
@@ -507,13 +507,13 @@
val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
(these_operations thy [class]);
- val c' = Sign.full_name thy' c;
+ val c' = Sign.full_bname thy' c;
val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
val rhs'' = map_types Logic.varifyT rhs';
val ty' = Term.fastype_of rhs';
in
thy'
- |> Sign.add_abbrev (#1 prmode) pos (Name.binding c, map_types Type.strip_sorts rhs'') |> snd
+ |> Sign.add_abbrev (#1 prmode) pos (Binding.name c, map_types Type.strip_sorts rhs'') |> snd
|> Sign.add_const_constraint (c', SOME ty')
|> Sign.notation true prmode [(Const (c', ty'), mx)]
|> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
@@ -574,14 +574,14 @@
val raw_params = (snd o chop (length supparams)) all_params;
fun add_const (v, raw_ty) thy =
let
- val c = Sign.full_name thy v;
+ val c = Sign.full_bname thy v;
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
val ty0 = Type.strip_sorts ty;
val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
in
thy
- |> Sign.declare_const [] ((Name.binding v, ty0), syn)
+ |> Sign.declare_const [] ((Binding.name v, ty0), syn)
|> snd
|> pair ((v, ty), (c, ty'))
end;
@@ -609,7 +609,7 @@
|> add_consts bname class base_sort sups supparams global_syntax
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
- [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
+ [((Binding.name (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
#> snd
#> `get_axiom
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
@@ -618,7 +618,7 @@
fun gen_class prep_spec bname raw_supclasses raw_elems thy =
let
- val class = Sign.full_name thy bname;
+ val class = Sign.full_bname thy bname;
val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
prep_spec thy raw_supclasses raw_elems;
val supconsts = map (apsnd fst o snd) (these_params thy sups);
--- a/src/Pure/Isar/constdefs.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/constdefs.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/constdefs.ML
- ID: $Id$
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
Old-style constant definitions, with type-inference and optional
@@ -9,12 +8,12 @@
signature CONSTDEFS =
sig
- val add_constdefs: (Name.binding * string option) list *
- ((Name.binding * string option * mixfix) option *
+ val add_constdefs: (Binding.T * string option) list *
+ ((Binding.T * string option * mixfix) option *
(Attrib.binding * string)) list -> theory -> theory
- val add_constdefs_i: (Name.binding * typ option) list *
- ((Name.binding * typ option * mixfix) option *
- ((Name.binding * attribute list) * term)) list -> theory -> theory
+ val add_constdefs_i: (Binding.T * typ option) list *
+ ((Binding.T * typ option * mixfix) option *
+ ((Binding.T * attribute list) * term)) list -> theory -> theory
end;
structure Constdefs: CONSTDEFS =
@@ -46,7 +45,7 @@
err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
else ());
- val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
+ val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
val name = Thm.def_name_optional c (Name.name_of raw_name);
val atts = map (prep_att thy) raw_atts;
--- a/src/Pure/Isar/element.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/element.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/element.ML
- ID: $Id$
Author: Makarius
Explicit data structures for some Isar language elements, with derived
@@ -10,11 +9,11 @@
sig
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list
+ Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list
type statement = (string, string) stmt
type statement_i = (typ, term) stmt
datatype ('typ, 'term, 'fact) ctxt =
- Fixes of (Name.binding * 'typ option * mixfix) list |
+ Fixes of (Binding.T * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
@@ -24,8 +23,8 @@
val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
(Attrib.binding * ('fact * Attrib.src list) list) list ->
(Attrib.binding * ('c * Attrib.src list) list) list
- val map_ctxt: {name: Name.binding -> Name.binding,
- var: Name.binding * mixfix -> Name.binding * mixfix,
+ val map_ctxt: {binding: Binding.T -> Binding.T,
+ var: Binding.T * mixfix -> Binding.T * mixfix,
typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
@@ -56,7 +55,7 @@
val rename_var_name: (string * (string * mixfix option)) list ->
string * mixfix -> string * mixfix
val rename_var: (string * (string * mixfix option)) list ->
- Name.binding * mixfix -> Name.binding * mixfix
+ Binding.T * mixfix -> Binding.T * mixfix
val rename_term: (string * (string * mixfix option)) list -> term -> term
val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
val rename_morphism: (string * (string * mixfix option)) list -> morphism
@@ -76,9 +75,9 @@
(Attrib.binding * (thm list * Attrib.src list) list) list ->
(Attrib.binding * (thm list * Attrib.src list) list) list
val activate: (typ, term, Facts.ref) ctxt list -> Proof.context ->
- (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
+ (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
val activate_i: context_i list -> Proof.context ->
- (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
+ (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
end;
structure Element: ELEMENT =
@@ -90,7 +89,7 @@
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list;
+ Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list;
type statement = (string, string) stmt;
type statement_i = (typ, term) stmt;
@@ -99,7 +98,7 @@
(* context *)
datatype ('typ, 'term, 'fact) ctxt =
- Fixes of (Name.binding * 'typ option * mixfix) list |
+ Fixes of (Binding.T * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
@@ -110,23 +109,23 @@
fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
-fun map_ctxt {name, var, typ, term, fact, attrib} =
+fun map_ctxt {binding, var, typ, term, fact, attrib} =
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
- let val x' = Name.name_of (#1 (var (Name.binding x, NoSyn))) in (x', typ T) end))
+ let val x' = Name.name_of (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
- ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
+ ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
- ((name a, map attrib atts), (term t, map term ps))))
+ ((binding a, map attrib atts), (term t, map term ps))))
| Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
- ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
+ ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
fun map_ctxt_attrib attrib =
- map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
+ map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
fun morph_ctxt phi = map_ctxt
- {name = Morphism.name phi,
+ {binding = Morphism.binding phi,
var = Morphism.var phi,
typ = Morphism.typ phi,
term = Morphism.term phi,
@@ -138,7 +137,7 @@
fun params_of (Fixes fixes) = fixes |> map
(fn (x, SOME T, _) => (Name.name_of x, T)
- | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.display x), []))
+ | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
| params_of _ = [];
fun prems_of (Assumes asms) = maps (map fst o snd) asms
@@ -163,7 +162,7 @@
fun pretty_name_atts ctxt (b, atts) sep =
let
- val name = Name.display b;
+ val name = Binding.display b;
in if name = "" andalso null atts then []
else [Pretty.block
(Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
@@ -212,7 +211,7 @@
Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
| prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
Pretty.brk 1 :: prt_mixfix mx);
- fun prt_constrain (x, T) = prt_fix (Name.binding x, SOME T, NoSyn);
+ fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
fun prt_asm (a, ts) =
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
@@ -246,13 +245,13 @@
else Pretty.command kind
in Pretty.block (Pretty.fbreaks (head :: prts)) end;
-fun fix (x, T) = (Name.binding x, SOME T);
+fun fix (x, T) = (Binding.name x, SOME T);
fun obtain prop ctxt =
let
val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
val As = Logic.strip_imp_prems (Thm.term_of prop');
- in ((Name.no_binding, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
+ in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
in
@@ -275,9 +274,9 @@
val (assumes, cases) = take_suffix (fn prem =>
is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
in
- pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) fixes)) @
- pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.no_binding, [(t, [])])) assumes)) @
- (if null cases then pretty_stmt ctxt' (Shows [(Attrib.no_binding, [(concl, [])])])
+ pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
+ pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
+ (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
else
let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
in pretty_stmt ctxt'' (Obtains clauses) end)
@@ -398,7 +397,7 @@
let
val x = Name.name_of b;
val (x', mx') = rename_var_name ren (x, mx);
- in (Name.binding x', mx') end;
+ in (Binding.name x', mx') end;
fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
| rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
@@ -419,7 +418,7 @@
end;
fun rename_morphism ren = Morphism.morphism
- {name = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
+ {binding = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
(* instantiate types *)
@@ -447,7 +446,7 @@
fun instT_morphism thy env =
let val thy_ref = Theory.check_thy thy in
Morphism.morphism
- {name = I, var = I,
+ {binding = I, var = I,
typ = instT_type env,
term = instT_term env,
fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)}
@@ -496,7 +495,7 @@
fun inst_morphism thy envs =
let val thy_ref = Theory.check_thy thy in
Morphism.morphism
- {name = I, var = I,
+ {binding = I, var = I,
typ = instT_type (#1 envs),
term = inst_term envs,
fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
@@ -528,7 +527,7 @@
val exp_term = Drule.term_rule thy (singleton exp_fact);
val exp_typ = Logic.type_map exp_term;
val morphism =
- Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+ Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in facts_map (morph_ctxt morphism) facts end;
@@ -553,7 +552,7 @@
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = LocalDefs.cert_def ctxt t
- in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+ in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
val (_, ctxt') =
ctxt |> fold (Variable.auto_fixes o #1) asms
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
@@ -577,7 +576,7 @@
fun prep_facts prep_name get intern ctxt elem = elem |> map_ctxt
{var = I, typ = I, term = I,
- name = Name.map_name prep_name,
+ binding = Binding.map_base prep_name,
fact = get ctxt,
attrib = intern (ProofContext.theory_of ctxt)};
--- a/src/Pure/Isar/expression.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/expression.ML Thu Dec 04 09:12:41 2008 -0800
@@ -8,8 +8,8 @@
sig
datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
type 'term expr = (string * (string * 'term map)) list;
- type expression = string expr * (Name.binding * string option * mixfix) list;
- type expression_i = term expr * (Name.binding * typ option * mixfix) list;
+ type expression = string expr * (Binding.T * string option * mixfix) list;
+ type expression_i = term expr * (Binding.T * typ option * mixfix) list;
(* Processing of context statements *)
val read_statement: Element.context list -> (string * string list) list list ->
@@ -47,8 +47,8 @@
type 'term expr = (string * (string * 'term map)) list;
-type expression = string expr * (Name.binding * string option * mixfix) list;
-type expression_i = term expr * (Name.binding * typ option * mixfix) list;
+type expression = string expr * (Binding.T * string option * mixfix) list;
+type expression_i = term expr * (Binding.T * typ option * mixfix) list;
(** Parsing and printing **)
@@ -164,7 +164,7 @@
(* FIXME: should check for bindings being the same.
Instead we check for equal name and syntax. *)
if mx1 = mx2 then mx1
- else error ("Conflicting syntax for parameter" ^ quote (Name.display p) ^
+ else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^
" in expression.")) (ps, ps')
in (i', ps'') end) is []
in (ps', is') end;
@@ -228,7 +228,7 @@
val inst = Symtab.make insts'';
in
(Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
- Morphism.name_morphism (Name.qualified prfx), ctxt')
+ Morphism.binding_morphism (Binding.qualify prfx), ctxt')
end;
@@ -237,7 +237,7 @@
(** Parsing **)
fun parse_elem prep_typ prep_term ctxt elem =
- Element.map_ctxt {name = I, var = I, typ = prep_typ ctxt,
+ Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt,
term = prep_term ctxt, fact = I, attrib = I} elem;
fun parse_concl prep_term ctxt concl =
@@ -316,7 +316,7 @@
let val (vars, _) = prep_vars fixes ctxt
in ctxt |> ProofContext.add_fixes_i vars |> snd end
| declare_elem prep_vars (Constrains csts) ctxt =
- ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd
+ ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
| declare_elem _ (Assumes _) ctxt = ctxt
| declare_elem _ (Defines _) ctxt = ctxt
| declare_elem _ (Notes _) ctxt = ctxt;
@@ -397,10 +397,10 @@
val defs' = map (Morphism.term morph) defs;
val text' = text |>
(if is_some asm
- then eval_text ctxt false (Assumes [(Attrib.no_binding, [(the asm', [])])])
+ then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
else I) |>
(if not (null defs)
- then eval_text ctxt false (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs'))
+ then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
else I)
(* FIXME clone from new_locale.ML *)
in ((loc, morph), text') end;
@@ -580,7 +580,7 @@
val exp_term = Drule.term_rule thy (singleton exp_fact);
val exp_typ = Logic.type_map exp_term;
val export' =
- Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+ Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in ((propss, deps, export'), goal_ctxt) end;
in
@@ -634,7 +634,7 @@
fun def_pred bname parms defs ts norm_ts thy =
let
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
val env = Term.add_term_free_names (body, []);
@@ -651,7 +651,7 @@
val ([pred_def], defs_thy) =
thy
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
- |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
+ |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
[((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
@@ -693,7 +693,7 @@
|> Sign.add_path aname
|> Sign.no_base_names
|> PureThy.note_thmss Thm.internalK
- [((Name.binding introN, []), [([intro], [NewLocale.unfold_attrib])])]
+ [((Binding.name introN, []), [([intro], [NewLocale.unfold_attrib])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
val (b_pred, b_intro, b_axioms, thy'''') =
@@ -708,8 +708,8 @@
|> Sign.add_path pname
|> Sign.no_base_names
|> PureThy.note_thmss Thm.internalK
- [((Name.binding introN, []), [([intro], [NewLocale.intro_attrib])]),
- ((Name.binding axiomsN, []),
+ [((Binding.name introN, []), [([intro], [NewLocale.intro_attrib])]),
+ ((Binding.name axiomsN, []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
||> Sign.restore_naming thy''';
in (SOME statement, SOME intro, axioms, thy'''') end;
@@ -741,7 +741,7 @@
bname predicate_name raw_imprt raw_body thy =
let
val thy_ctxt = ProofContext.init thy;
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
val _ = NewLocale.test_locale thy name andalso
error ("Duplicate definition of locale " ^ quote name);
@@ -765,7 +765,7 @@
fst |> map (Element.morph_ctxt satisfy) |>
map_filter (fn Notes notes => SOME notes | _ => NONE) |>
(if is_some asm
- then cons (Thm.internalK, [((Name.binding (bname ^ "_" ^ axiomsN), []),
+ then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
[([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
else I);
--- a/src/Pure/Isar/isar_cmd.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/isar_cmd.ML Thu Dec 04 09:12:41 2008 -0800
@@ -14,8 +14,8 @@
val typed_print_translation: bool * (string * Position.T) -> theory -> theory
val print_ast_translation: bool * (string * Position.T) -> theory -> theory
val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
- val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
- val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
+ val add_axioms: ((Binding.T * string) * Attrib.src list) list -> theory -> theory
+ val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory
val declaration: string * Position.T -> local_theory -> local_theory
val simproc_setup: string -> string list -> string * Position.T -> string list ->
local_theory -> local_theory
--- a/src/Pure/Isar/isar_syn.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/isar_syn.ML Thu Dec 04 09:12:41 2008 -0800
@@ -272,7 +272,7 @@
val _ =
OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
(P.and_list1 SpecParse.xthms1
- >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.no_binding, flat args)]));
+ >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
(* name space entry path *)
@@ -396,7 +396,7 @@
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
-val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
+val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
val _ =
OuterSyntax.command "sublocale"
@@ -483,7 +483,7 @@
fun gen_theorem kind =
OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
(Scan.optional (SpecParse.opt_thm_name ":" --|
- Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.no_binding --
+ Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
SpecParse.general_statement >> (fn (a, (elems, concl)) =>
(Specification.theorem_cmd kind NONE (K I) a elems concl)));
--- a/src/Pure/Isar/local_defs.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/local_defs.ML Thu Dec 04 09:12:41 2008 -0800
@@ -12,10 +12,10 @@
val mk_def: Proof.context -> (string * term) list -> term list
val expand: cterm list -> thm -> thm
val def_export: Assumption.export
- val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
+ val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
Proof.context -> (term * (string * thm)) list * Proof.context
- val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
- val fixed_abbrev: (Name.binding * mixfix) * term -> Proof.context ->
+ val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+ val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
(term * term) * Proof.context
val export: Proof.context -> Proof.context -> thm -> thm list * thm
val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
@@ -92,7 +92,7 @@
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
val xs = map Name.name_of bvars;
- val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
+ val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
in
@@ -105,7 +105,7 @@
end;
fun add_def (var, rhs) ctxt =
- let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
+ let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
in ((lhs, th), ctxt') end;
--- a/src/Pure/Isar/local_theory.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/local_theory.ML Thu Dec 04 09:12:41 2008 -0800
@@ -26,9 +26,9 @@
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val affirm: local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
- val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
+ val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -56,10 +56,10 @@
type operations =
{pretty: local_theory -> Pretty.T list,
- abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
+ abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
(term * term) * local_theory,
define: string ->
- (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory,
notes: string ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -142,7 +142,7 @@
|> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
|> NameSpace.qualified_names;
-val full_name = NameSpace.full o full_naming;
+fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name;
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
|> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
--- a/src/Pure/Isar/locale.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/locale.ML Thu Dec 04 09:12:41 2008 -0800
@@ -92,10 +92,10 @@
(* Storing results *)
val global_note_qualified: string ->
- ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+ ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
theory -> (string * thm list) list * theory
val local_note_qualified: string ->
- ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+ ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
Proof.context -> Proof.context
@@ -104,11 +104,11 @@
val add_declaration: string -> declaration -> Proof.context -> Proof.context
(* Interpretation *)
- val get_interpret_morph: theory -> (Name.binding -> Name.binding) -> string * string ->
+ val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string ->
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
string -> term list -> Morphism.morphism
val interpretation: (Proof.context -> Proof.context) ->
- (Name.binding -> Name.binding) -> expr ->
+ (Binding.T -> Binding.T) -> expr ->
term option list * (Attrib.binding * term) list ->
theory ->
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
@@ -117,7 +117,7 @@
val interpretation_in_locale: (Proof.context -> Proof.context) ->
xstring * expr -> theory -> Proof.state
val interpret: (Proof.state -> Proof.state Seq.seq) ->
- (Name.binding -> Name.binding) -> expr ->
+ (Binding.T -> Binding.T) -> expr ->
term option list * (Attrib.binding * term) list ->
bool -> Proof.state ->
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
@@ -226,7 +226,7 @@
(** management of registrations in theories and proof contexts **)
type registration =
- {prfx: (Name.binding -> Name.binding) * (string * string),
+ {prfx: (Binding.T -> Binding.T) * (string * string),
(* first component: interpretation name morphism;
second component: parameter prefix *)
exp: Morphism.morphism,
@@ -248,18 +248,18 @@
val join: T * T -> T
val dest: theory -> T ->
(term list *
- (((Name.binding -> Name.binding) * (string * string)) *
+ (((Binding.T -> Binding.T) * (string * string)) *
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
Element.witness list *
thm Termtab.table)) list
val test: theory -> T * term list -> bool
val lookup: theory ->
T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
- (((Name.binding -> Name.binding) * (string * string)) * Element.witness list * thm Termtab.table) option
- val insert: theory -> term list -> ((Name.binding -> Name.binding) * (string * string)) ->
+ (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option
+ val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) ->
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
T ->
- T * (term list * (((Name.binding -> Name.binding) * (string * string)) * Element.witness list)) list
+ T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list
val add_witness: term list -> Element.witness -> T -> T
val add_equation: term list -> thm -> T -> T
(*
@@ -433,7 +433,8 @@
fun register_locale name loc thy =
thy |> LocalesData.map (fn (space, locs) =>
- (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
+ (NameSpace.declare_base (Sign.naming_of thy) name space,
+ Symtab.update (name, loc) locs));
fun change_locale name f thy =
let
@@ -811,7 +812,7 @@
fun make_raw_params_elemss (params, tenv, syn) =
[((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
Int [Fixes (map (fn p =>
- (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
+ (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
(* flatten_expr:
@@ -954,7 +955,7 @@
#> Binding.add_prefix false lprfx;
val elem_morphism =
Element.rename_morphism ren $>
- Morphism.name_morphism add_prefices $>
+ Morphism.binding_morphism add_prefices $>
Element.instT_morphism thy env;
val elems' = map (Element.morph_ctxt elem_morphism) elems;
in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
@@ -1003,7 +1004,7 @@
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = LocalDefs.cert_def ctxt t
- in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+ in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
val (_, ctxt') =
ctxt |> fold (Variable.auto_fixes o #1) asms
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
@@ -1129,7 +1130,7 @@
let val (vars, _) = prep_vars fixes ctxt
in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
| declare_ext_elem prep_vars (Constrains csts) ctxt =
- let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
+ let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt
in ([], ctxt') end
| declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
| declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
@@ -1412,7 +1413,7 @@
|> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
| prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
{var = I, typ = I, term = I,
- name = Name.map_name prep_name,
+ binding = Binding.map_base prep_name,
fact = get ctxt,
attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
@@ -1637,9 +1638,9 @@
fun name_morph phi_name (lprfx, pprfx) b =
b
- |> (if not (Binding.is_nothing b) andalso pprfx <> ""
+ |> (if not (Binding.is_empty b) andalso pprfx <> ""
then Binding.add_prefix false pprfx else I)
- |> (if not (Binding.is_nothing b)
+ |> (if not (Binding.is_empty b)
then Binding.add_prefix false lprfx else I)
|> phi_name;
@@ -1651,9 +1652,9 @@
(* FIXME sync with exp_fact *)
val exp_typ = Logic.type_map exp_term;
val export' =
- Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+ Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in
- Morphism.name_morphism (name_morph phi_name param_prfx) $>
+ Morphism.binding_morphism (name_morph phi_name param_prfx) $>
Element.inst_morphism thy insts $>
Element.satisfy_morphism prems $>
Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
@@ -1732,7 +1733,7 @@
(fn (axiom, elems, params, decls, regs, intros, dests) =>
(axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
add_thmss loc Thm.internalK
- [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+ [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
in
@@ -1789,7 +1790,7 @@
fun def_pred bname parms defs ts norm_ts thy =
let
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
val env = Term.add_term_free_names (body, []);
@@ -1806,7 +1807,7 @@
val ([pred_def], defs_thy) =
thy
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
- |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
+ |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
[((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
@@ -1876,12 +1877,12 @@
|> def_pred aname parms defs exts exts';
val elemss' = change_assumes_elemss axioms elemss;
val a_elem = [(("", []),
- [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
+ [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
val (_, thy'') =
thy'
|> Sign.add_path aname
|> Sign.no_base_names
- |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
+ |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])]
||> Sign.restore_naming thy';
in ((elemss', [statement]), a_elem, [intro], thy'') end;
val (predicate, stmt', elemss'', b_intro, thy'''') =
@@ -1894,14 +1895,14 @@
val cstatement = Thm.cterm_of thy''' statement;
val elemss'' = change_elemss_hyps axioms elemss';
val b_elem = [(("", []),
- [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
+ [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
val (_, thy'''') =
thy'''
|> Sign.add_path pname
|> Sign.no_base_names
|> PureThy.note_thmss Thm.internalK
- [((Name.binding introN, []), [([intro], [])]),
- ((Name.binding axiomsN, []),
+ [((Binding.name introN, []), [([intro], [])]),
+ ((Binding.name axiomsN, []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
||> Sign.restore_naming thy''';
in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
@@ -1918,7 +1919,7 @@
fun defines_to_notes is_ext thy (Defines defs) defns =
let
- val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
+ val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs
val notes = map (fn (a, (def, _)) =>
(a, [([assume (cterm_of thy def)], [])])) defs
in
@@ -1940,7 +1941,7 @@
"name" - locale with predicate named "name" *)
let
val thy_ctxt = ProofContext.init thy;
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
val _ = is_some (get_locale thy name) andalso
error ("Duplicate definition of locale " ^ quote name);
@@ -2007,9 +2008,9 @@
end;
val _ = Context.>> (Context.map_theory
- (add_locale "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
+ (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #>
snd #> ProofContext.theory_of #>
- add_locale "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
+ add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #>
snd #> ProofContext.theory_of));
@@ -2378,7 +2379,7 @@
fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
let
val att_morphism =
- Morphism.name_morphism (name_morph phi_name param_prfx) $>
+ Morphism.binding_morphism (name_morph phi_name param_prfx) $>
Morphism.thm_morphism satisfy $>
Element.inst_morphism thy insts $>
Morphism.thm_morphism disch;
@@ -2438,13 +2439,13 @@
in
state
|> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
- "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
+ "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss))
|> Element.refine_witness |> Seq.hd
|> pair morphs
end;
fun standard_name_morph interp_prfx b =
- if Binding.is_nothing b then b
+ if Binding.is_empty b then b
else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
fold (Binding.add_prefix false o fst) pprfx
#> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
--- a/src/Pure/Isar/new_locale.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/new_locale.ML Thu Dec 04 09:12:41 2008 -0800
@@ -11,7 +11,7 @@
val clear_idents: Proof.context -> Proof.context
val test_locale: theory -> string -> bool
val register_locale: string ->
- (string * sort) list * (Name.binding * typ option * mixfix) list ->
+ (string * sort) list * (Binding.T * typ option * mixfix) list ->
term option * term list ->
(declaration * stamp) list * (declaration * stamp) list ->
((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
@@ -22,7 +22,7 @@
val extern: theory -> string -> xstring
(* Specification *)
- val params_of: theory -> string -> (Name.binding * typ option * mixfix) list
+ val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
val specification_of: theory -> string -> term option * term list
val declarations_of: theory -> string -> declaration list * declaration list
@@ -84,7 +84,7 @@
datatype locale = Loc of {
(* extensible lists are in reverse order: decls, notes, dependencies *)
- parameters: (string * sort) list * (Name.binding * typ option * mixfix) list,
+ parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
(* type and term parameters *)
spec: term option * term list,
(* assumptions (as a single predicate expression) and defines *)
@@ -138,7 +138,7 @@
fun register_locale name parameters spec decls notes dependencies thy =
thy |> LocalesData.map (fn (space, locs) =>
- (Sign.declare_name thy name space, Symtab.update (name,
+ (NameSpace.declare_base (Sign.naming_of thy) name space, Symtab.update (name,
Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
dependencies = dependencies}) locs));
@@ -279,9 +279,9 @@
input |>
(if not (null params) then activ_elem (Fixes params) else I) |>
(* FIXME type parameters *)
- (if is_some asm then activ_elem (Assumes [(Attrib.no_binding, [(the asm, [])])]) else I) |>
+ (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
(if not (null defs)
- then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
+ then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
else I) |>
pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
end;
@@ -366,7 +366,7 @@
(fn (parameters, spec, decls, notes, dependencies) =>
(parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
add_thmss loc Thm.internalK
- [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+ [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
in
--- a/src/Pure/Isar/object_logic.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/object_logic.ML Thu Dec 04 09:12:41 2008 -0800
@@ -89,7 +89,7 @@
fun typedecl (raw_name, vs, mx) thy =
let
val base_sort = get_base_sort thy;
- val name = Sign.full_name thy (Syntax.type_name raw_name mx);
+ val name = Sign.full_bname thy (Syntax.type_name raw_name mx);
val _ = has_duplicates (op =) vs andalso
error ("Duplicate parameters in type declaration: " ^ quote name);
val n = length vs;
@@ -107,7 +107,7 @@
local
fun gen_add_judgment add_consts (bname, T, mx) thy =
- let val c = Sign.full_name thy (Syntax.const_name bname mx) in
+ let val c = Sign.full_bname thy (Syntax.const_name bname mx) in
thy
|> add_consts [(bname, T, mx)]
|> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
--- a/src/Pure/Isar/obtain.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/obtain.ML Thu Dec 04 09:12:41 2008 -0800
@@ -40,16 +40,16 @@
signature OBTAIN =
sig
val thatN: string
- val obtain: string -> (Name.binding * string option * mixfix) list ->
+ val obtain: string -> (Binding.T * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
- ((Name.binding * attribute list) * (term * term list) list) list ->
+ val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
+ ((Binding.T * attribute list) * (term * term list) list) list ->
bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
(cterm list * thm list) * Proof.context
- val guess: (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val guess_i: (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
@@ -156,14 +156,14 @@
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K Seq.single) [((Name.no_binding, []), [(obtain_prop, [])])] int
+ |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
- |> Proof.fix_i [(Name.binding thesisN, NONE, NoSyn)]
+ |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume_i
- [((Name.binding that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
+ [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show_i NONE after_qed [((Name.no_binding, []), [(thesis, [])])] false
+ ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false
|-> Proof.refine_insert
end;
@@ -294,9 +294,9 @@
in
state'
|> Proof.map_context (K ctxt')
- |> Proof.fix_i (map (fn ((x, T), mx) => (Name.binding x, SOME T, mx)) parms)
+ |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
- (obtain_export fix_ctxt rule (map cert ts)) [((Name.no_binding, []), asms)])
+ (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)])
|> Proof.add_binds_i AutoBind.no_facts
end;
@@ -311,10 +311,10 @@
state
|> Proof.enter_forward
|> Proof.begin_block
- |> Proof.fix_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)]
+ |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
- "guess" before_qed after_qed [((Name.no_binding, []), [Logic.mk_term goal, goal])]
+ "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])]
|> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
end;
--- a/src/Pure/Isar/outer_parse.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/outer_parse.ML Thu Dec 04 09:12:41 2008 -0800
@@ -61,12 +61,12 @@
val list: (token list -> 'a * token list) -> token list -> 'a list * token list
val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
val name: token list -> bstring * token list
- val binding: token list -> Name.binding * token list
+ val binding: token list -> Binding.T * token list
val xname: token list -> xstring * token list
val text: token list -> string * token list
val path: token list -> Path.T * token list
val parname: token list -> string * token list
- val parbinding: token list -> Name.binding * token list
+ val parbinding: token list -> Binding.T * token list
val sort: token list -> string * token list
val arity: token list -> (string * string list * string) * token list
val multi_arity: token list -> (string list * string list * string) * token list
@@ -81,11 +81,11 @@
val opt_mixfix': token list -> mixfix * token list
val where_: token list -> string * token list
val const: token list -> (string * string * mixfix) * token list
- val params: token list -> (Name.binding * string option) list * token list
- val simple_fixes: token list -> (Name.binding * string option) list * token list
- val fixes: token list -> (Name.binding * string option * mixfix) list * token list
- val for_fixes: token list -> (Name.binding * string option * mixfix) list * token list
- val for_simple_fixes: token list -> (Name.binding * string option) list * token list
+ val params: token list -> (Binding.T * string option) list * token list
+ val simple_fixes: token list -> (Binding.T * string option) list * token list
+ val fixes: token list -> (Binding.T * string option * mixfix) list * token list
+ val for_fixes: token list -> (Binding.T * string option * mixfix) list * token list
+ val for_simple_fixes: token list -> (Binding.T * string option) list * token list
val ML_source: token list -> (SymbolPos.text * Position.T) * token list
val doc_source: token list -> (SymbolPos.text * Position.T) * token list
val properties: token list -> Properties.T * token list
@@ -228,13 +228,13 @@
(* names and text *)
val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Binding.binding_pos;
+val binding = position name >> Binding.name_pos;
val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
val path = group "file name/path specification" name >> Path.explode;
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
-val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Name.no_binding;
+val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
(* sorts and arities *)
--- a/src/Pure/Isar/proof.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/proof.ML Thu Dec 04 09:12:41 2008 -0800
@@ -45,27 +45,27 @@
val match_bind_i: (term list * term) list -> state -> state
val let_bind: (string list * string) list -> state -> state
val let_bind_i: (term list * term) list -> state -> state
- val fix: (Name.binding * string option * mixfix) list -> state -> state
- val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
+ val fix: (Binding.T * string option * mixfix) list -> state -> state
+ val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
val assm: Assumption.export ->
(Attrib.binding * (string * string list) list) list -> state -> state
val assm_i: Assumption.export ->
- ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
+ ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
val assume: (Attrib.binding * (string * string list) list) list -> state -> state
- val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
+ val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
state -> state
val presume: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
+ val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
state -> state
- val def: (Attrib.binding * ((Name.binding * mixfix) * (string * string list))) list ->
+ val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
state -> state
- val def_i: ((Name.binding * attribute list) *
- ((Name.binding * mixfix) * (term * term list))) list -> state -> state
+ val def_i: ((Binding.T * attribute list) *
+ ((Binding.T * mixfix) * (term * term list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: ((Name.binding * attribute list) *
+ val note_thmss_i: ((Binding.T * attribute list) *
(thm list * attribute list) list) list -> state -> state
val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
@@ -89,7 +89,7 @@
(theory -> 'a -> attribute) ->
(context * 'b list -> context * (term list list * (context -> context))) ->
string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((Name.binding * 'a list) * 'b) list -> state -> state
+ ((Binding.T * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state Seq.seq
val theorem: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
@@ -109,11 +109,11 @@
val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+ ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
val is_relevant: state -> bool
val future_proof: (state -> context) -> state -> context
end;
@@ -617,7 +617,7 @@
(* note etc. *)
-fun no_binding args = map (pair (Name.no_binding, [])) args;
+fun no_binding args = map (pair (Binding.empty, [])) args;
local
@@ -645,7 +645,7 @@
val local_results =
gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
-fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
+fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
end;
@@ -689,14 +689,14 @@
val atts = map (prep_att (theory_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
- val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
+ val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts));
in
state'
|> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
|> assume_i assumptions
|> add_binds_i AutoBind.no_facts
|> map_context (ProofContext.restore_naming (context_of state))
- |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
+ |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
end;
in
@@ -1002,7 +1002,7 @@
val statement' = (kind, [[], [Thm.term_of cprop_protected]], cprop_protected);
val goal' = Thm.adjust_maxidx_thm ~1 (Drule.protectI RS Goal.init cprop_protected);
fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
- val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
+ val this_name = ProofContext.full_bname (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
fun make_result () = state
|> map_contexts (Variable.auto_fixes prop)
--- a/src/Pure/Isar/proof_context.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/proof_context.ML Thu Dec 04 09:12:41 2008 -0800
@@ -23,8 +23,8 @@
val abbrev_mode: Proof.context -> bool
val set_stmt: bool -> Proof.context -> Proof.context
val naming_of: Proof.context -> NameSpace.naming
- val full_name: Proof.context -> bstring -> string
- val full_binding: Proof.context -> Name.binding -> string
+ val full_name: Proof.context -> Binding.T -> string
+ val full_bname: Proof.context -> bstring -> string
val consts_of: Proof.context -> Consts.T
val const_syntax_name: Proof.context -> string -> string
val the_const_constraint: Proof.context -> string -> typ
@@ -105,27 +105,27 @@
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
val note_thmss: string ->
- ((Name.binding * attribute list) * (Facts.ref * attribute list) list) list ->
+ ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val note_thmss_i: string ->
- ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
+ ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
- val read_vars: (Name.binding * string option * mixfix) list -> Proof.context ->
- (Name.binding * typ option * mixfix) list * Proof.context
- val cert_vars: (Name.binding * typ option * mixfix) list -> Proof.context ->
- (Name.binding * typ option * mixfix) list * Proof.context
- val add_fixes: (Name.binding * string option * mixfix) list ->
+ val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
+ (Binding.T * typ option * mixfix) list * Proof.context
+ val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
+ (Binding.T * typ option * mixfix) list * Proof.context
+ val add_fixes: (Binding.T * string option * mixfix) list ->
Proof.context -> string list * Proof.context
- val add_fixes_i: (Name.binding * typ option * mixfix) list ->
+ val add_fixes_i: (Binding.T * typ option * mixfix) list ->
Proof.context -> string list * Proof.context
val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
val add_assms: Assumption.export ->
- ((Name.binding * attribute list) * (string * string list) list) list ->
+ ((Binding.T * attribute list) * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_assms_i: Assumption.export ->
- ((Name.binding * attribute list) * (term * term list) list) list ->
+ ((Binding.T * attribute list) * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -135,7 +135,7 @@
Context.generic -> Context.generic
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> Properties.T ->
- Name.binding * term -> Proof.context -> (term * term) * Proof.context
+ Binding.T * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
val verbose: bool ref
val setmp_verbose: ('a -> 'b) -> 'a -> 'b
@@ -247,8 +247,8 @@
val naming_of = #naming o rep_context;
-val full_name = NameSpace.full o naming_of;
-val full_binding = NameSpace.full_binding o naming_of;
+val full_name = NameSpace.full_name o naming_of;
+fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
val syntax_of = #syntax o rep_context;
val syn_of = LocalSyntax.syn_of o syntax_of;
@@ -965,14 +965,14 @@
local
-fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
+fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
| update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
(Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
let
val pos = Binding.pos_of b;
- val name = full_binding ctxt b;
+ val name = full_name ctxt b;
val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
@@ -991,7 +991,7 @@
fun put_thms do_props thms ctxt = ctxt
|> map_naming (K local_naming)
|> ContextPosition.set_visible false
- |> update_thms do_props (apfst Name.binding thms)
+ |> update_thms do_props (apfst Binding.name thms)
|> ContextPosition.restore_visible ctxt
|> restore_naming ctxt;
@@ -1021,7 +1021,7 @@
if internal then T
else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
- val var = (Name.map_name (K x) raw_b, opt_T, mx);
+ val var = (Binding.map_base (K x) raw_b, opt_T, mx);
in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
in
@@ -1095,7 +1095,7 @@
fun add_abbrev mode tags (b, raw_t) ctxt =
let
val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
- handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
+ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
val ((lhs, rhs), consts') = consts_of ctxt
|> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
@@ -1146,7 +1146,7 @@
fun bind_fixes xs ctxt =
let
- val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Name.binding x, NONE, NoSyn)) xs);
+ val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
fun bind (t as Free (x, T)) =
if member (op =) xs x then
(case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
--- a/src/Pure/Isar/rule_insts.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/rule_insts.ML Thu Dec 04 09:12:41 2008 -0800
@@ -284,7 +284,7 @@
val (param_names, ctxt') = ctxt
|> Variable.declare_thm thm
|> Thm.fold_terms Variable.declare_constraints st
- |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params);
+ |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
(* Process type insts: Tinsts_env *)
fun absent xi = error
--- a/src/Pure/Isar/spec_parse.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/spec_parse.ML Thu Dec 04 09:12:41 2008 -0800
@@ -15,14 +15,14 @@
val opt_thm_name: string -> token list -> Attrib.binding * token list
val spec: token list -> (Attrib.binding * string list) * token list
val named_spec: token list -> (Attrib.binding * string list) * token list
- val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
- val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
+ val spec_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
+ val spec_opt_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
val xthm: token list -> (Facts.ref * Attrib.src list) * token list
val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
val name_facts: token list ->
(Attrib.binding * (Facts.ref * Attrib.src list) list) list * token list
val locale_mixfix: token list -> mixfix * token list
- val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
+ val locale_fixes: token list -> (Binding.T * string option * mixfix) list * token list
val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
val class_expr: token list -> string list * token list
val locale_expr: token list -> Locale.expr * token list
@@ -33,8 +33,8 @@
(Element.context list * Element.statement) * OuterLex.token list
val statement_keyword: token list -> string * token list
val specification: token list ->
- (Name.binding *
- ((Attrib.binding * string list) list * (Name.binding * string option) list)) list * token list
+ (Binding.T *
+ ((Attrib.binding * string list) list * (Binding.T * string option) list)) list * token list
end;
structure SpecParse: SPEC_PARSE =
@@ -53,8 +53,8 @@
fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
fun opt_thm_name s =
- Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
- Attrib.no_binding;
+ Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
+ Attrib.empty_binding;
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
--- a/src/Pure/Isar/specification.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/specification.ML Thu Dec 04 09:12:41 2008 -0800
@@ -9,33 +9,33 @@
signature SPECIFICATION =
sig
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
- val check_specification: (Name.binding * typ option * mixfix) list ->
+ val check_specification: (Binding.T * typ option * mixfix) list ->
(Attrib.binding * term list) list list -> Proof.context ->
- (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_specification: (Name.binding * string option * mixfix) list ->
+ (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val read_specification: (Binding.T * string option * mixfix) list ->
(Attrib.binding * string list) list list -> Proof.context ->
- (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val check_free_specification: (Name.binding * typ option * mixfix) list ->
+ (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val check_free_specification: (Binding.T * typ option * mixfix) list ->
(Attrib.binding * term list) list -> Proof.context ->
- (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val read_free_specification: (Name.binding * string option * mixfix) list ->
+ (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val read_free_specification: (Binding.T * string option * mixfix) list ->
(Attrib.binding * string list) list -> Proof.context ->
- (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
- val axiomatization: (Name.binding * typ option * mixfix) list ->
+ (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+ val axiomatization: (Binding.T * typ option * mixfix) list ->
(Attrib.binding * term list) list -> theory ->
(term list * (string * thm list) list) * theory
- val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
+ val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
(Attrib.binding * string list) list -> theory ->
(term list * (string * thm list) list) * theory
val definition:
- (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
+ (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory
val definition_cmd:
- (Name.binding * string option * mixfix) option * (Attrib.binding * string) ->
+ (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
local_theory -> (term * (string * thm)) * local_theory
- val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
+ val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
local_theory -> local_theory
- val abbreviation_cmd: Syntax.mode -> (Name.binding * string option * mixfix) option * string ->
+ val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
@@ -181,10 +181,10 @@
val (vars, [((raw_name, atts), [prop])]) =
fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
- val name = Name.map_name (Thm.def_name_optional x) raw_name;
+ val name = Binding.map_base (Thm.def_name_optional x) raw_name;
val var =
(case vars of
- [] => (Name.binding x, NoSyn)
+ [] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
val y = Name.name_of b;
@@ -193,7 +193,7 @@
Position.str_of (Binding.pos_of b));
in (b, mx) end);
val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
- (var, ((Name.map_name (suffix "_raw") name, []), rhs));
+ (var, ((Binding.map_base (suffix "_raw") name, []), rhs));
val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
@@ -217,7 +217,7 @@
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
val var =
(case vars of
- [] => (Name.binding x, NoSyn)
+ [] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
val y = Name.name_of b;
@@ -312,13 +312,13 @@
val atts = map (Attrib.internal o K)
[RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
val prems = subtract_prems ctxt elems_ctxt;
- val stmt = [((Name.no_binding, atts), [(thesis, [])])];
+ val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)])
+ |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
- [((Name.binding Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+ [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
in ((prems, stmt, facts), goal_ctxt) end);
structure TheoremHook = GenericDataFun
@@ -348,7 +348,7 @@
lthy
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>
- if Binding.is_nothing name andalso null atts then
+ if Binding.is_empty name andalso null atts then
(ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
else
let
@@ -361,7 +361,7 @@
in
goal_ctxt
|> ProofContext.note_thmss_i Thm.assumptionK
- [((Name.binding AutoBind.assmsN, []), [(prems, [])])]
+ [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
|> Proof.refine_insert facts
--- a/src/Pure/Isar/theory_target.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Isar/theory_target.ML Thu Dec 04 09:12:41 2008 -0800
@@ -59,9 +59,9 @@
let
val thy = ProofContext.theory_of ctxt;
val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
- val fixes = map (fn (x, T) => (Name.binding x, SOME T, NoSyn))
+ val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
(#1 (ProofContext.inferred_fixes ctxt));
- val assumes = map (fn A => (Attrib.no_binding, [(Thm.term_of A, [])]))
+ val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
(Assumption.assms_of ctxt);
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
@@ -195,13 +195,13 @@
fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
let
- val b' = Morphism.name phi b;
+ val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
val arg = (b', Term.close_schematic_term rhs');
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
- val (prefix', _) = Binding.dest_binding b';
+ val (prefix', _) = Binding.dest b';
val class_global = Name.name_of b = Name.name_of b'
andalso not (null prefix')
andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
@@ -292,7 +292,7 @@
val thy_ctxt = ProofContext.init thy;
val c = Name.name_of b;
- val name' = Name.map_name (Thm.def_name_optional c) name;
+ val name' = Binding.map_base (Thm.def_name_optional c) name;
val (rhs', rhs_conv) =
LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
--- a/src/Pure/ROOT.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/ROOT.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/ROOT.ML
- ID: $Id$
Pure Isabelle.
*)
--- a/src/Pure/Tools/invoke.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/Tools/invoke.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/Tools/invoke.ML
- ID: $Id$
Author: Makarius
Schematic invocation of locale expression in proof context.
@@ -8,9 +7,9 @@
signature INVOKE =
sig
val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
- (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
val invoke_i: string * attribute list -> Locale.expr -> term option list ->
- (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Invoke: INVOKE =
@@ -60,9 +59,9 @@
| NONE => Drule.termI)) params';
val propp =
- [((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
- ((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'),
- ((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')];
+ [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
+ ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'),
+ ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')];
fun after_qed results =
Proof.end_block #>
Proof.map_context (fn ctxt =>
--- a/src/Pure/assumption.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/assumption.ML Thu Dec 04 09:12:41 2008 -0800
@@ -120,6 +120,6 @@
val thm = export false inner outer;
val term = export_term inner outer;
val typ = Logic.type_map term;
- in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end;
+ in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end;
end;
--- a/src/Pure/axclass.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/axclass.ML Thu Dec 04 09:12:41 2008 -0800
@@ -9,7 +9,7 @@
signature AX_CLASS =
sig
val define_class: bstring * class list -> string list ->
- ((Name.binding * attribute list) * term list) list -> theory -> class * theory
+ ((Binding.T * attribute list) * term list) list -> theory -> class * theory
val add_classrel: thm -> theory -> theory
val add_arity: thm -> theory -> theory
val prove_classrel: class * class -> tactic -> theory -> theory
@@ -370,7 +370,7 @@
thy
|> Sign.sticky_prefix name_inst
|> Sign.no_base_names
- |> Sign.declare_const [] ((Name.binding c', T'), NoSyn)
+ |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
|-> (fn const' as Const (c'', _) => Thm.add_def false true
(Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
@@ -422,7 +422,7 @@
(* class *)
val bconst = Logic.const_of_class bclass;
- val class = Sign.full_name thy bclass;
+ val class = Sign.full_bname thy bclass;
val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
fun check_constraint (a, S) =
@@ -482,9 +482,9 @@
|> Sign.add_path bconst
|> Sign.no_base_names
|> PureThy.note_thmss ""
- [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
- ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
- ((Name.binding axiomsN, []),
+ [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
+ ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
+ ((Binding.name axiomsN, []),
[(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
||> Sign.restore_naming def_thy;
@@ -530,7 +530,7 @@
fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
let
- val class = Sign.full_name thy bclass;
+ val class = Sign.full_bname thy bclass;
val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
in
thy
--- a/src/Pure/consts.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/consts.ML Thu Dec 04 09:12:41 2008 -0800
@@ -30,10 +30,10 @@
val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
- val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * typ) -> T -> T
+ val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
val constrain: string * typ option -> T -> T
val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
- Name.binding * term -> T -> (term * term) * T
+ Binding.T * term -> T -> (term * term) * T
val revert_abbrev: string -> string -> T -> T
val hide: bool -> string -> T -> T
val empty: T
@@ -211,7 +211,7 @@
fun err_dup_const c =
error ("Duplicate declaration of constant " ^ quote c);
-fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab
+fun extend_decls naming decl tab = NameSpace.bind naming decl tab
handle Symtab.DUP c => err_dup_const c;
@@ -273,7 +273,7 @@
|> cert_term;
val normal_rhs = expand_term rhs;
val T = Term.fastype_of rhs;
- val lhs = Const (NameSpace.full_binding naming b, T);
+ val lhs = Const (NameSpace.full_name naming b, T);
fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
--- a/src/Pure/facts.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/facts.ML Thu Dec 04 09:12:41 2008 -0800
@@ -31,9 +31,9 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: NameSpace.naming -> Name.binding * thm list -> T -> string * T
- val add_local: bool -> NameSpace.naming -> Name.binding * thm list -> T -> string * T
- val add_dynamic: NameSpace.naming -> Name.binding * (Context.generic -> thm list) -> T -> string * T
+ val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
+ val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
+ val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
end;
@@ -192,10 +192,10 @@
fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
let
- val (name, facts') = if Binding.is_nothing b then ("", facts)
+ val (name, facts') = if Binding.is_empty b then ("", facts)
else let
val (space, tab) = facts;
- val (name, space') = NameSpace.declare_binding naming b space;
+ val (name, space') = NameSpace.declare naming b space;
val entry = (name, (Static ths, serial ()));
val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
handle Symtab.DUP dup => err_dup_fact dup;
@@ -213,7 +213,7 @@
fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
let
- val (name, space') = NameSpace.declare_binding naming b space;
+ val (name, space') = NameSpace.declare naming b space;
val entry = (name, (Dynamic f, serial ()));
val tab' = Symtab.update_new entry tab
handle Symtab.DUP dup => err_dup_fact dup;
--- a/src/Pure/more_thm.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/more_thm.ML Thu Dec 04 09:12:41 2008 -0800
@@ -281,7 +281,7 @@
let
val name' = if name = "" then "axiom_" ^ serial_string () else name;
val thy' = thy |> Theory.add_axioms_i [(name', prop)];
- val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' name'));
+ val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name'));
in (axm, thy') end;
fun add_def unchecked overloaded (name, prop) thy =
@@ -293,7 +293,7 @@
val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
- val axm' = Thm.axiom thy' (Sign.full_name thy' name);
+ val axm' = Thm.axiom thy' (Sign.full_bname thy' name);
val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
in (thm, thy') end;
--- a/src/Pure/morphism.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/morphism.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Pure/morphism.ML
- ID: $Id$
Author: Makarius
Abstract morphisms on formal entities.
@@ -17,21 +16,21 @@
signature MORPHISM =
sig
include BASIC_MORPHISM
- val var: morphism -> Name.binding * mixfix -> Name.binding * mixfix
- val name: morphism -> Name.binding -> Name.binding
+ val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
+ val binding: morphism -> Binding.T -> Binding.T
val typ: morphism -> typ -> typ
val term: morphism -> term -> term
val fact: morphism -> thm list -> thm list
val thm: morphism -> thm -> thm
val cterm: morphism -> cterm -> cterm
val morphism:
- {name: Name.binding -> Name.binding,
- var: Name.binding * mixfix -> Name.binding * mixfix,
+ {binding: Binding.T -> Binding.T,
+ var: Binding.T * mixfix -> Binding.T * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list} -> morphism
- val name_morphism: (Name.binding -> Name.binding) -> morphism
- val var_morphism: (Name.binding * mixfix -> Name.binding * mixfix) -> morphism
+ val binding_morphism: (Binding.T -> Binding.T) -> morphism
+ val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
val typ_morphism: (typ -> typ) -> morphism
val term_morphism: (term -> term) -> morphism
val fact_morphism: (thm list -> thm list) -> morphism
@@ -46,15 +45,15 @@
struct
datatype morphism = Morphism of
- {name: Name.binding -> Name.binding,
- var: Name.binding * mixfix -> Name.binding * mixfix,
+ {binding: Binding.T -> Binding.T,
+ var: Binding.T * mixfix -> Binding.T * mixfix,
typ: typ -> typ,
term: term -> term,
fact: thm list -> thm list};
type declaration = morphism -> Context.generic -> Context.generic;
-fun name (Morphism {name, ...}) = name;
+fun binding (Morphism {binding, ...}) = binding;
fun var (Morphism {var, ...}) = var;
fun typ (Morphism {typ, ...}) = typ;
fun term (Morphism {term, ...}) = term;
@@ -64,19 +63,19 @@
val morphism = Morphism;
-fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I};
-fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I};
-fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, fact = I};
-fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, fact = I};
-fun fact_morphism fact = morphism {name = I, var = I, typ = I, term = I, fact = fact};
-fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, fact = map thm};
+fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
+fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
+fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
+fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
+fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
+fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
-val identity = morphism {name = I, var = I, typ = I, term = I, fact = I};
+val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
fun compose
- (Morphism {name = name1, var = var1, typ = typ1, term = term1, fact = fact1})
- (Morphism {name = name2, var = var2, typ = typ2, term = term2, fact = fact2}) =
- morphism {name = name1 o name2, var = var1 o var2,
+ (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
+ (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
+ morphism {binding = binding1 o binding2, var = var1 o var2,
typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
fun phi1 $> phi2 = compose phi2 phi1;
--- a/src/Pure/name.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/name.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,8 +1,7 @@
(* Title: Pure/name.ML
- ID: $Id$
Author: Makarius
-Names of basic logical entities (variables etc.). Generic name bindings.
+Names of basic logical entities (variables etc.).
*)
signature NAME =
@@ -29,11 +28,7 @@
val variant_list: string list -> string list -> string list
val variant: string list -> string -> string
- include BINDING
- type binding = Binding.T
val name_of: Binding.T -> string (*FIMXE legacy*)
- val map_name: (string -> string) -> Binding.T -> Binding.T (*FIMXE legacy*)
- val qualified: string -> Binding.T -> Binding.T (*FIMXE legacy*)
end;
structure Name: NAME =
@@ -146,15 +141,8 @@
fun variant used = singleton (variant_list used);
-(** generic name bindings **)
-
-open Binding;
+(** generic name bindings -- legacy **)
-type binding = Binding.T;
-
-val prefix_of = fst o dest_binding;
-val name_of = snd o dest_binding;
-val map_name = map_binding o apsnd;
-val qualified = map_name o NameSpace.qualified;
+val name_of = snd o Binding.dest;
end;
--- a/src/Pure/pure_thy.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/pure_thy.ML Thu Dec 04 09:12:41 2008 -0800
@@ -31,9 +31,9 @@
val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
- val note_thmss: string -> ((Name.binding * attribute list) *
+ val note_thmss: string -> ((Binding.T * attribute list) *
(thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
- val note_thmss_grouped: string -> string -> ((Name.binding * attribute list) *
+ val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) *
(thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
@@ -144,11 +144,11 @@
(FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
fun enter_thms pre_name post_name app_att (b, thms) thy =
- if Binding.is_nothing b
+ if Binding.is_empty b
then swap (enter_proofs (app_att (thy, thms)))
else let
val naming = Sign.naming_of thy;
- val name = NameSpace.full_binding naming b;
+ val name = NameSpace.full_name naming b;
val (thy', thms') =
enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
val thms'' = map (Thm.transfer thy') thms';
@@ -159,20 +159,20 @@
(* store_thm(s) *)
fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
- (name_thms false true Position.none) I (Name.binding bname, thms);
+ (name_thms false true Position.none) I (Binding.name bname, thms);
fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
fun store_thm_open (bname, th) =
enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
- (Name.binding bname, [th]) #>> the_single;
+ (Binding.name bname, [th]) #>> the_single;
(* add_thms(s) *)
fun add_thms_atts pre_name ((bname, thms), atts) =
enter_thms pre_name (name_thms false true Position.none)
- (foldl_map (Thm.theory_attributes atts)) (Name.binding bname, thms);
+ (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms);
fun gen_add_thmss pre_name =
fold_map (add_thms_atts pre_name);
@@ -189,7 +189,7 @@
fun add_thms_dynamic (bname, f) thy = thy
|> (FactsData.map o apfst)
- (Facts.add_dynamic (Sign.naming_of thy) (Name.binding bname, f) #> snd);
+ (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd);
(* note_thmss *)
@@ -199,7 +199,7 @@
fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
let
val pos = Binding.pos_of b;
- val name = Sign.full_binding thy b;
+ val name = Sign.full_name thy b;
val _ = Position.report (Markup.fact_decl name) pos;
fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
@@ -219,7 +219,7 @@
(* store axioms as theorems *)
local
- fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_name thy name);
+ fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name);
fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
let
--- a/src/Pure/sign.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/sign.ML Thu Dec 04 09:12:41 2008 -0800
@@ -14,11 +14,10 @@
tsig: Type.tsig,
consts: Consts.T}
val naming_of: theory -> NameSpace.naming
+ val full_name: theory -> Binding.T -> string
val base_name: string -> bstring
- val full_name: theory -> bstring -> string
- val full_binding: theory -> Name.binding -> string
- val full_name_path: theory -> string -> bstring -> string
- val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
+ val full_bname: theory -> bstring -> string
+ val full_bname_path: theory -> string -> bstring -> string
val syn_of: theory -> Syntax.syntax
val tsig_of: theory -> Type.tsig
val classes_of: theory -> Sorts.algebra
@@ -92,10 +91,10 @@
val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
- val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
+ val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
val add_consts: (bstring * string * mixfix) list -> theory -> theory
val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
- val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory
+ val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
val revert_abbrev: string -> string -> theory -> theory
val add_const_constraint: string * typ option -> theory -> theory
val primitive_class: string * class list -> theory -> theory
@@ -189,10 +188,10 @@
val naming_of = #naming o rep_sg;
val base_name = NameSpace.base;
-val full_name = NameSpace.full o naming_of;
-val full_binding = NameSpace.full_binding o naming_of;
-fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
-val declare_name = NameSpace.declare o naming_of;
+val full_name = NameSpace.full_name o naming_of;
+fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
+fun full_bname_path thy elems =
+ NameSpace.full_name (NameSpace.add_path elems (naming_of thy)) o Binding.name;
(* syntax *)
@@ -510,11 +509,11 @@
fun prep (raw_b, raw_T, raw_mx) =
let
val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
- val b = Name.map_name (K mx_name) raw_b;
- val c = full_binding thy b;
+ val b = Binding.map_base (K mx_name) raw_b;
+ val c = full_name thy b;
val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
- cat_error msg ("in declaration of constant " ^ quote (Name.display b));
+ cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
val T' = Logic.varifyT T;
in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
val args = map prep raw_args;
@@ -526,7 +525,7 @@
|> pair (map #3 args)
end;
-fun bindify (name, T, mx) = (Name.binding name, T, mx);
+fun bindify (name, T, mx) = (Binding.name name, T, mx);
in
@@ -551,7 +550,7 @@
val pp = Syntax.pp_global thy;
val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
- handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
+ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
val (res, consts') = consts_of thy
|> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
in (res, thy |> map_consts (K consts')) end;
--- a/src/Pure/simplifier.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/simplifier.ML Thu Dec 04 09:12:41 2008 -0800
@@ -194,11 +194,11 @@
in
lthy |> LocalTheory.declaration (fn phi =>
let
- val b' = Morphism.name phi (Name.binding name);
+ val b' = Morphism.binding phi (Binding.name name);
val simproc' = morph_simproc phi simproc;
in
Simprocs.map (fn simprocs =>
- NameSpace.table_declare naming (b', simproc') simprocs |> snd
+ NameSpace.bind naming (b', simproc') simprocs |> snd
handle Symtab.DUP dup => err_dup_simproc dup)
#> map_ss (fn ss => ss addsimprocs [simproc'])
end)
--- a/src/Pure/theory.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/theory.ML Thu Dec 04 09:12:41 2008 -0800
@@ -36,7 +36,7 @@
val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
val add_finals: bool -> string list -> theory -> theory
val add_finals_i: bool -> term list -> theory -> theory
- val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
+ val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
end
structure Theory: THEORY =
@@ -253,7 +253,7 @@
fun check_def thy unchecked overloaded (bname, tm) defs =
let
val ctxt = ProofContext.init thy;
- val name = Sign.full_name thy bname;
+ val name = Sign.full_bname thy bname;
val (lhs_const, rhs) = Sign.cert_def ctxt tm;
val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
val _ = check_overloading thy overloaded lhs_const;
--- a/src/Pure/thm.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/thm.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1732,9 +1732,9 @@
fun add_oracle (bname, oracle) thy =
let
val naming = Sign.naming_of thy;
- val name = NameSpace.full naming bname;
+ val name = NameSpace.full_name naming (Binding.name bname);
val thy' = thy |> Oracles.map (fn (space, tab) =>
- (NameSpace.declare naming name space,
+ (NameSpace.declare_base naming name space,
Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
--- a/src/Pure/type.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/type.ML Thu Dec 04 09:12:41 2008 -0800
@@ -509,10 +509,10 @@
fun add_class pp naming (c, cs) tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
- val c' = NameSpace.full naming c;
+ val c' = NameSpace.full_name naming (Binding.name c);
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
- val space' = space |> NameSpace.declare naming c';
+ val space' = space |> NameSpace.declare_base naming c';
val classes' = classes |> Sorts.add_class pp (c', cs');
in ((space', classes'), default, types) end);
@@ -568,8 +568,8 @@
fun new_decl naming tags (c, decl) (space, types) =
let
val tags' = tags |> Position.default_properties (Position.thread_data ());
- val c' = NameSpace.full naming c;
- val space' = NameSpace.declare naming c' space;
+ val c' = NameSpace.full_name naming (Binding.name c);
+ val space' = NameSpace.declare_base naming c' space;
val types' =
(case Symtab.lookup types c' of
SOME ((decl', _), _) => err_in_decls c' decl decl'
--- a/src/Pure/variable.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Pure/variable.ML Thu Dec 04 09:12:41 2008 -0800
@@ -398,7 +398,7 @@
val fact = export inner outer;
val term = singleton (export_terms inner outer);
val typ = Logic.type_map term;
- in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = fact} end;
+ in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = fact} end;
--- a/src/Tools/induct.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/Tools/induct.ML Thu Dec 04 09:12:41 2008 -0800
@@ -1,5 +1,4 @@
(* Title: Tools/induct.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Proof by cases, induction, and coinduction.
@@ -51,7 +50,7 @@
val setN: string
(*proof methods*)
val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
- val add_defs: (Name.binding option * term) option list -> Proof.context ->
+ val add_defs: (Binding.T option * term) option list -> Proof.context ->
(term option list * thm list) * Proof.context
val atomize_term: theory -> term -> term
val atomize_tac: int -> tactic
@@ -63,7 +62,7 @@
val cases_tac: Proof.context -> term option list list -> thm option ->
thm list -> int -> cases_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
- val induct_tac: Proof.context -> (Name.binding option * term) option list list ->
+ val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
@@ -553,7 +552,7 @@
let
fun add (SOME (SOME x, t)) ctxt =
let val ([(lhs, (_, th))], ctxt') =
- LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
+ LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
| add NONE ctxt = ((NONE, []), ctxt);
--- a/src/ZF/Tools/datatype_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/ZF/Tools/datatype_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -101,7 +101,7 @@
val npart = length rec_names; (*number of mutually recursive parts*)
- val full_name = Sign.full_name thy_path;
+ val full_name = Sign.full_bname thy_path;
(*Make constructor definition;
kpart is the number of this mutually recursive part*)
@@ -262,7 +262,7 @@
||> add_recursor
||> Sign.parent_path
- val intr_names = map (Name.binding o #2) (List.concat con_ty_lists);
+ val intr_names = map (Binding.name o #2) (List.concat con_ty_lists);
val (thy1, ind_result) =
thy0 |> Ind_Package.add_inductive_i
false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
--- a/src/ZF/Tools/inductive_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/ZF/Tools/inductive_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -29,10 +29,10 @@
(*Insert definitions for the recursive sets, which
must *already* be declared as constants in parent theory!*)
val add_inductive_i: bool -> term list * term ->
- ((Name.binding * term) * attribute list) list ->
+ ((Binding.T * term) * attribute list) list ->
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
- ((Name.binding * string) * Attrib.src list) list ->
+ ((Binding.T * string) * Attrib.src list) list ->
(Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
(Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
theory -> theory * inductive_result
--- a/src/ZF/Tools/primrec_package.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/ZF/Tools/primrec_package.ML Thu Dec 04 09:12:41 2008 -0800
@@ -9,8 +9,8 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec: ((Name.binding * string) * Attrib.src list) list -> theory -> theory * thm list
- val add_primrec_i: ((Name.binding * term) * attribute list) list -> theory -> theory * thm list
+ val add_primrec: ((Binding.T * string) * Attrib.src list) list -> theory -> theory * thm list
+ val add_primrec_i: ((Binding.T * term) * attribute list) list -> theory -> theory * thm list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
--- a/src/ZF/ind_syntax.ML Thu Dec 04 08:47:45 2008 -0800
+++ b/src/ZF/ind_syntax.ML Thu Dec 04 09:12:41 2008 -0800
@@ -85,7 +85,7 @@
Logic.list_implies
(map FOLogic.mk_Trueprop prems,
FOLogic.mk_Trueprop
- (@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args)
+ (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
$ rec_tm))
in map mk_intr constructs end;