# HG changeset patch # User huffman # Date 1228410761 28800 # Node ID 1c743f58781af2f6873ec273d0e8c1d234c78729 # Parent 4ed63cdda7993df235278c76b06a09d64ef65245# Parent 71a7f76b522d8014156add25e55c9ace09b9c2f4 merged. diff -r 4ed63cdda799 -r 1c743f58781a NEWS --- 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. diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Code_Eval.thy --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Import/hol4rews.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Import/proof_kernel.ML --- 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) diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/List.thy --- 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 *} diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Nominal/Nominal.thy --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Nominal/nominal_atoms.ML --- 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_-type together with -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_-type together with -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 -combination a cp___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_ *) 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]; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Nominal/nominal_induct.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Nominal/nominal_inductive2.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Nominal/nominal_package.ML --- 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'')))); diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Nominal/nominal_primrec.ML --- 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 = diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Statespace/state_space.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/datatype_abs_proofs.ML --- 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))) @ diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/datatype_codegen.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/datatype_package.ML --- 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 ^ diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/datatype_rep_proofs.ML --- 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 *) diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/fundef_common.ML --- 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, diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/fundef_core.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/fundef_lib.ML --- 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" diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/inductive_wrap.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/mutual.ML --- 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, diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/function_package/size.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/inductive_package.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/inductive_realizer.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/inductive_set_package.ML --- 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) = diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/primrec_package.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/recdef_package.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/record_package.ML --- 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]; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/res_axioms.ML --- 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*) diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/typecopy_package.ML --- 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 [] diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Tools/typedef_package.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Typedef.thy --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/Typerep.thy --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/ex/Quickcheck.thy --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/HOL/ex/Term_Of_Syntax.thy --- 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 \ 'b"}), NoSyn) + Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \ 'b"}), NoSyn) #> snd *} diff -r 4ed63cdda799 -r 1c743f58781a src/HOLCF/Tools/domain/domain_axioms.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOLCF/Tools/domain/domain_extender.ML --- 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); diff -r 4ed63cdda799 -r 1c743f58781a src/HOLCF/Tools/domain/domain_theorems.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/HOLCF/Tools/fixrec_package.ML --- 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 = diff -r 4ed63cdda799 -r 1c743f58781a src/HOLCF/Tools/pcpodef_package.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/General/binding.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/General/name_space.ML --- 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)); diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/args.ML --- 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, []); diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/attrib.ML --- 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), diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/calculation.ML --- 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 *) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/class.ML --- 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); diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/constdefs.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/element.ML --- 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)}; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/expression.ML --- 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); diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/isar_cmd.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/isar_syn.ML --- 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))); diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/local_defs.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/local_theory.ML --- 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)) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/locale.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/new_locale.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/object_logic.ML --- 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') diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/obtain.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/outer_parse.ML --- 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 *) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/proof.ML --- 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) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/proof_context.ML --- 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) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/rule_insts.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/spec_parse.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/specification.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Isar/theory_target.ML --- 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' []; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/ROOT.ML --- 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. *) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/Tools/invoke.ML --- 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 => diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/assumption.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/axclass.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/consts.ML --- 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))); diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/facts.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/more_thm.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/morphism.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/name.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/pure_thy.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/sign.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/simplifier.ML --- 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) diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/theory.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/thm.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/type.ML --- 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' diff -r 4ed63cdda799 -r 1c743f58781a src/Pure/variable.ML --- 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; diff -r 4ed63cdda799 -r 1c743f58781a src/Tools/induct.ML --- 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); diff -r 4ed63cdda799 -r 1c743f58781a src/ZF/Tools/datatype_package.ML --- 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)) diff -r 4ed63cdda799 -r 1c743f58781a src/ZF/Tools/inductive_package.ML --- 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 diff -r 4ed63cdda799 -r 1c743f58781a src/ZF/Tools/primrec_package.ML --- 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 = diff -r 4ed63cdda799 -r 1c743f58781a src/ZF/ind_syntax.ML --- 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;