# HG changeset patch # User haftmann # Date 1232558863 -3600 # Node ID c23295521af5ae4d8dcece7fe256ab3adb1d84b6 # Parent 88ba5e5ac6d84c35e67493f39cca8e16f0bc5235 binding replaces bstring diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Import/hol4rews.ML Wed Jan 21 18:27:43 2009 +0100 @@ -390,7 +390,7 @@ val thm2 = standard thm1; in thy - |> PureThy.store_thm (bthm, thm2) + |> PureThy.store_thm (Binding.name bthm, thm2) |> snd |> add_hol4_theorem bthy bthm hth end; diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Import/proof_kernel.ML Wed Jan 21 18:27:43 2009 +0100 @@ -1928,7 +1928,7 @@ Replaying _ => thy | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy) val eq = mk_defeq constname rhs' thy1 - val (thms, thy2) = PureThy.add_defs false [((thmname,eq),[])] thy1 + val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1 val _ = ImportRecorder.add_defs thmname eq val def_thm = hd thms val thm' = def_thm RS meta_eq_to_obj_eq_thm diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Import/replay.ML Wed Jan 21 18:27:43 2009 +0100 @@ -340,7 +340,7 @@ | delta (Hol_move (fullname, moved_thmname)) thy = add_hol4_move fullname moved_thmname thy | delta (Defs (thmname, eq)) thy = - snd (PureThy.add_defs false [((thmname, eq), [])] thy) + snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy) | delta (Hol_theorem (thyname, thmname, th)) thy = add_hol4_theorem thyname thmname ([], th_of thy th) thy | delta (Typedef (thmname, typ, c, repabs, th)) thy = diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jan 21 18:27:43 2009 +0100 @@ -90,6 +90,9 @@ let val T = fastype_of x in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end; +fun add_thms_string args = PureThy.add_thms ((map o apfst o apfst) Binding.name args); +fun add_thmss_string args = PureThy.add_thmss ((map o apfst o apfst) Binding.name args); + (* this function sets up all matters related to atom- *) (* kinds; the user specifies a list of atom-kind names *) (* atom_decl ... *) @@ -121,7 +124,7 @@ atac 1] val (inj_thm,thy2) = - PureThy.add_thms [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1 + add_thms_string [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1 (* second statement *) val y = Free ("y",ak_type) @@ -136,7 +139,7 @@ (* third statement *) val (inject_thm,thy3) = - PureThy.add_thms [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2 + add_thms_string [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2 val stmnt3 = HOLogic.mk_Trueprop (HOLogic.mk_not @@ -152,7 +155,7 @@ simp_tac (HOL_basic_ss addsimps simp3) 1] val (inf_thm,thy4) = - PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3 + add_thms_string [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3 in ((inj_thm,inject_thm,inf_thm),thy4) end) ak_names thy @@ -186,7 +189,7 @@ val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) in thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] - |> PureThy.add_defs_unchecked true [((name, def2),[])] + |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])] |> snd |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])] end) ak_names_types thy1; @@ -241,14 +244,14 @@ val def = Logic.mk_equals (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a) in - PureThy.add_defs_unchecked true [((name, def),[])] thy' + PureThy.add_defs_unchecked true [((Binding.name name, def),[])] thy' end) ak_names_types thy) ak_names_types thy4; (* proves that every atom-kind is an instance of at *) (* lemma at__inst: *) (* at TYPE() *) val (prm_cons_thms,thy6) = - thy5 |> PureThy.add_thms (map (fn (ak_name, T) => + thy5 |> add_thms_string (map (fn (ak_name, T) => let val ak_name_qu = Sign.full_bname thy5 (ak_name); val i_type = Type(ak_name_qu,[]); @@ -309,7 +312,7 @@ (* lemma pt__inst: *) (* pt TYPE('x::pt_) TYPE() *) val (prm_inst_thms,thy8) = - thy7 |> PureThy.add_thms (map (fn (ak_name, T) => + thy7 |> add_thms_string (map (fn (ak_name, T) => let val ak_name_qu = Sign.full_bname thy7 ak_name; val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name); @@ -355,7 +358,7 @@ (* lemma abst__inst: *) (* fs TYPE('x::pt_) TYPE () *) val (fs_inst_thms,thy12) = - thy11 |> PureThy.add_thms (map (fn (ak_name, T) => + thy11 |> add_thms_string (map (fn (ak_name, T) => let val ak_name_qu = Sign.full_bname thy11 ak_name; val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name); @@ -428,7 +431,7 @@ rtac allI 1, rtac allI 1, rtac allI 1, rtac cp1 1]; in - yield_singleton PureThy.add_thms ((name, + yield_singleton add_thms_string ((name, Goal.prove_global thy' [] [] statement proof), []) thy' end) ak_names_types thy) ak_names_types thy12b; @@ -460,7 +463,7 @@ val proof = fn _ => simp_tac simp_s 1; in - PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' + add_thms_string [((name, Goal.prove_global thy' [] [] statement proof), [])] thy' end else ([],thy'))) (* do nothing branch, if ak_name = ak_name' *) @@ -870,114 +873,114 @@ fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms); in thy32 - |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] - ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])] - ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])] - ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])] - ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] - ||>> PureThy.add_thmss + |> add_thmss_string [(("alpha", inst_pt_at [abs_fun_eq]),[])] + ||>> add_thmss_string [(("alpha'", inst_pt_at [abs_fun_eq']),[])] + ||>> add_thmss_string [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])] + ||>> add_thmss_string [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])] + ||>> add_thmss_string [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] + ||>> add_thmss_string let val thms1 = inst_at at_swap_simps and thms2 = inst_dj [dj_perm_forget] in [(("swap_simps", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [pt_pi_rev]; val thms2 = inst_pt_at [pt_rev_pi]; in [(("perm_pi_simp",thms1 @ thms2),[])] end - ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] - ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])] - ||>> PureThy.add_thmss + ||>> add_thmss_string [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] + ||>> add_thmss_string [(("perm_bij", inst_pt_at [pt_bij]),[])] + ||>> add_thmss_string let val thms1 = inst_pt_at [pt_perm_compose]; val thms2 = instR cp1 (Library.flat cps'); in [(("perm_compose",thms1 @ thms2),[])] end - ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] - ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])] - ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] - ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])] - ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])] - ||>> PureThy.add_thmss + ||>> add_thmss_string [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] + ||>> add_thmss_string [(("perm_app", inst_pt_at [perm_app]),[])] + ||>> add_thmss_string [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])] + ||>> add_thmss_string [(("exists_fresh", inst_at [at_exists_fresh]),[])] + ||>> add_thmss_string [(("exists_fresh'", inst_at [at_exists_fresh']),[])] + ||>> add_thmss_string let val thms1 = inst_pt_at [all_eqvt]; val thms2 = map (fold_rule [inductive_forall_def]) thms1 in [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])] end - ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])] - ||>> PureThy.add_thmss [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])] - ||>> PureThy.add_thmss [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])] - ||>> PureThy.add_thmss + ||>> add_thmss_string [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])] + ||>> add_thmss_string [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])] + ||>> add_thmss_string [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])] + ||>> add_thmss_string let val thms1 = inst_at [at_fresh] val thms2 = inst_dj [at_fresh_ineq] in [(("fresh_atm", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_at at_calc and thms2 = inst_dj [dj_perm_forget] in [(("calc_atm", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [abs_fun_pi] and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_dj [dj_perm_forget] and thms2 = inst_dj [dj_pp_forget] in [(("perm_dj", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at_fs [fresh_iff] and thms2 = inst_pt_at [fresh_iff] and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq] in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [abs_fun_supp] and thms2 = inst_pt_at_fs [abs_fun_supp] and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq] in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_left] and thms2 = inst_pt_pt_at_cp [fresh_left_ineq] in [(("fresh_left", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_right] and thms2 = inst_pt_pt_at_cp [fresh_right_ineq] in [(("fresh_right", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_bij] and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] in [(("fresh_bij", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at fresh_star_bij and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq); in [(("fresh_star_bij", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_eqvt] and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq] in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [in_eqvt] in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [eq_eqvt] in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [set_diff_eqvt] in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [subseteq_eqvt] in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])] - ||>> PureThy.add_thmss [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])] - ||>> PureThy.add_thmss [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])] - ||>> PureThy.add_thmss + ||>> add_thmss_string [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])] + ||>> add_thmss_string [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])] + ||>> add_thmss_string [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])] + ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_aux] and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] in [(("fresh_aux", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_perm_app] and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] in [(("fresh_perm_app", thms1 @ thms2),[])] end - ||>> PureThy.add_thmss + ||>> add_thmss_string let val thms1 = inst_pt_at [pt_perm_supp] and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] in [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end - ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])] + ||>> add_thmss_string [(("fin_supp",fs_axs),[])] end; in diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jan 21 18:27:43 2009 +0100 @@ -562,17 +562,17 @@ [ind_case_names, RuleCases.consumes 1]); val ([strong_induct'], thy') = thy |> Sign.add_path rec_name |> - PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)]; + PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)]; val strong_inducts = ProjectRule.projects ctxt (1 upto length names) strong_induct' in thy' |> - PureThy.add_thmss [(("strong_inducts", strong_inducts), + PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts), [ind_case_names, RuleCases.consumes 1])] |> snd |> Sign.parent_path |> fold (fn ((name, elim), (_, cases)) => Sign.add_path (Sign.base_name name) #> - PureThy.add_thms [(("strong_cases", elim), + PureThy.add_thms [((Binding.name "strong_cases", elim), [RuleCases.case_names (map snd cases), RuleCases.consumes 1])] #> snd #> Sign.parent_path) (strong_cases ~~ induct_cases') @@ -653,7 +653,7 @@ in fold (fn (name, ths) => Sign.add_path (Sign.base_name name) #> - PureThy.add_thmss [(("eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #> + PureThy.add_thmss [((Binding.name "eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #> Sign.parent_path) (names ~~ transp thss) thy end; diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 21 18:27:43 2009 +0100 @@ -458,12 +458,12 @@ [ind_case_names, RuleCases.consumes 1]); val ([strong_induct'], thy') = thy |> Sign.add_path rec_name |> - PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)]; + PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)]; val strong_inducts = ProjectRule.projects ctxt (1 upto length names) strong_induct' in thy' |> - PureThy.add_thmss [(("strong_inducts", strong_inducts), + PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts), [ind_case_names, RuleCases.consumes 1])] |> snd |> Sign.parent_path end)) diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Wed Jan 21 18:27:43 2009 +0100 @@ -490,13 +490,13 @@ (full_new_type_names' ~~ tyvars) thy end) atoms |> PureThy.add_thmss - [((space_implode "_" new_type_names ^ "_unfolded_perm_eq", + [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"), unfolded_perm_eq_thms), [Simplifier.simp_add]), - ((space_implode "_" new_type_names ^ "_perm_empty", + ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"), perm_empty_thms), [Simplifier.simp_add]), - ((space_implode "_" new_type_names ^ "_perm_append", + ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"), perm_append_thms), [Simplifier.simp_add]), - ((space_implode "_" new_type_names ^ "_perm_eq", + ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"), perm_eq_thms), [Simplifier.simp_add])]; (**** Define representing sets ****) @@ -627,7 +627,7 @@ val pi = Free ("pi", permT); val T = Type (Sign.intern_type thy name, map TFree tvs); in apfst (pair r o hd) - (PureThy.add_defs_unchecked true [(("prm_" ^ name ^ "_def", Logic.mk_equals + (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T), Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $ (Const ("Nominal.perm", permT --> U --> U) $ pi $ @@ -801,7 +801,7 @@ val def_name = (Sign.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] |> - (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)] + (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] in (thy', defs @ [def_thm], eqns @ [eqn]) end; fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)), @@ -1114,8 +1114,8 @@ val (_, thy9) = thy8 |> Sign.add_path big_name |> - PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] ||>> - PureThy.add_thmss [(("inducts", projections dt_induct), [case_names_induct])] ||> + PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>> + PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||> Sign.parent_path ||>> DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>> DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>> @@ -1405,9 +1405,9 @@ val (_, thy10) = thy9 |> Sign.add_path big_name |> - PureThy.add_thms [(("strong_induct'", induct_aux), [])] ||>> - PureThy.add_thms [(("strong_induct", induct), [case_names_induct])] ||>> - PureThy.add_thmss [(("strong_inducts", projections induct), [case_names_induct])]; + PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>> + PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>> + PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])]; (**** recursion combinator ****) @@ -2015,7 +2015,7 @@ (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, + (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); @@ -2052,12 +2052,12 @@ (* FIXME: theorems are stored in database for testing only *) val (_, thy13) = thy12 |> PureThy.add_thmss - [(("rec_equiv", List.concat rec_equiv_thms), []), - (("rec_equiv'", List.concat rec_equiv_thms'), []), - (("rec_fin_supp", List.concat rec_fin_supp_thms), []), - (("rec_fresh", List.concat rec_fresh_thms), []), - (("rec_unique", map standard rec_unique_thms), []), - (("recs", rec_thms), [])] ||> + [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []), + ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []), + ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []), + ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []), + ((Binding.name "rec_unique", map standard rec_unique_thms), []), + ((Binding.name "recs", rec_thms), [])] ||> Sign.parent_path ||> map_nominal_datatypes (fold Symtab.update dt_infos); diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Jan 21 18:27:43 2009 +0100 @@ -187,8 +187,8 @@ "equivariance theorem declaration (without checking the form of the lemma)"), ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"), ("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")] #> - PureThy.add_thms_dynamic ("eqvts", #eqvts o Data.get) #> - PureThy.add_thms_dynamic ("freshs", #freshs o Data.get) #> - PureThy.add_thms_dynamic ("bijs", #bijs o Data.get); + PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #> + PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #> + PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get); end; diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Wed Jan 21 18:27:43 2009 +0100 @@ -111,10 +111,10 @@ fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy)); -fun add_axioms_i x = snd o PureThy.add_axioms (map Thm.no_attributes x); +fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; -fun add_defs_i x = snd o (PureThy.add_defs false) (map Thm.no_attributes x); +fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; in (* local *) diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Wed Jan 21 18:27:43 2009 +0100 @@ -134,7 +134,7 @@ in theorems_thy |> Sign.add_path (Sign.base_name comp_dnam) - |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])])) + |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) |> Sign.parent_path end; diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Jan 21 18:27:43 2009 +0100 @@ -607,7 +607,7 @@ in thy |> Sign.add_path (Sign.base_name dname) - |> (snd o (PureThy.add_thmss (map Thm.no_attributes [ + |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [ ("iso_rews" , iso_rews ), ("exhaust" , [exhaust] ), ("casedist" , [casedist]), @@ -623,7 +623,7 @@ ("injects" , injects ), ("copy_rews", copy_rews)]))) |> (snd o PureThy.add_thmss - [(("match_rews", mat_rews), [Simplifier.simp_add])]) + [((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])]) |> Sign.parent_path |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ pat_rews @ dist_les @ dist_eqs @ copy_rews) @@ -1000,7 +1000,7 @@ end; (* local *) in thy |> Sign.add_path comp_dnam - |> (snd o (PureThy.add_thmss (map Thm.no_attributes [ + |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [ ("take_rews" , take_rews ), ("take_lemmas", take_lemmas), ("finites" , finites ), diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOLCF/Tools/fixrec_package.ML Wed Jan 21 18:27:43 2009 +0100 @@ -96,7 +96,7 @@ val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs; val (fixdef_thms, thy') = - PureThy.add_defs false (map Thm.no_attributes fixdefs) thy; + PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) fixdefs) thy; val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms; val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss)); @@ -114,7 +114,7 @@ in (n^"_unfold", thmL) :: unfolds ns thmR end; val unfold_thms = unfolds names ctuple_unfold_thm; val thms = ctuple_induct_thm :: unfold_thms; - val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy'; + val (_, thy'') = PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name) thms) thy'; in (thy'', names, fixdef_thms, map snd unfold_thms) end; @@ -241,14 +241,14 @@ in if strict then let (* only prove simp rules if strict = true *) val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts); - val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks)); - val (simp_thms, thy'') = PureThy.add_thms simps thy'; + val simps = maps (make_simps thy') (unfold_thms ~~ eqn_blocks); + val (simp_thms, thy'') = PureThy.add_thms ((map o apfst o apfst) Binding.name simps) thy'; val simp_names = map (fn name => name^"_simps") cnames; val simp_attribute = rpair [Simplifier.simp_add]; val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms); in - (snd o PureThy.add_thmss simps') thy'' + (snd o PureThy.add_thmss ((map o apfst o apfst) Binding.name simps')) thy'' end else thy' end; @@ -278,7 +278,7 @@ val ts = map (prep_term thy) strings; val simps = map (fix_pat thy) ts; in - (snd o PureThy.add_thmss [((Binding.base_name name, simps), atts)]) thy + (snd o PureThy.add_thmss [((name, simps), atts)]) thy end; val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute; diff -r 88ba5e5ac6d8 -r c23295521af5 src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Wed Jan 21 16:51:45 2009 +0100 +++ b/src/HOLCF/Tools/pcpodef_package.ML Wed Jan 21 18:27:43 2009 +0100 @@ -97,12 +97,12 @@ theory' |> Sign.add_path name |> PureThy.add_thms - ([(("adm_" ^ name, admissible'), []), - (("cont_" ^ Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []), - (("cont_" ^ Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []), - (("lub_" ^ name, @{thm typedef_lub} OF cpo_thms'), []), - (("thelub_" ^ name, @{thm typedef_thelub} OF cpo_thms'), []), - (("compact_" ^ name, @{thm typedef_compact} OF cpo_thms'), [])]) + ([((Binding.name ("adm_" ^ name), admissible'), []), + ((Binding.name ("cont_" ^ Rep_name), @{thm typedef_cont_Rep} OF cpo_thms'), []), + ((Binding.name ("cont_" ^ Abs_name), @{thm typedef_cont_Abs} OF cpo_thms'), []), + ((Binding.name ("lub_" ^ name), @{thm typedef_lub} OF cpo_thms'), []), + ((Binding.name ("thelub_" ^ name), @{thm typedef_thelub} OF cpo_thms'), []), + ((Binding.name ("compact_" ^ name), @{thm typedef_compact} OF cpo_thms'), [])]) |> snd |> Sign.parent_path end; @@ -119,12 +119,12 @@ theory' |> Sign.add_path name |> PureThy.add_thms - ([((Rep_name ^ "_strict", @{thm typedef_Rep_strict} OF pcpo_thms'), []), - ((Abs_name ^ "_strict", @{thm typedef_Abs_strict} OF pcpo_thms'), []), - ((Rep_name ^ "_strict_iff", @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []), - ((Abs_name ^ "_strict_iff", @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []), - ((Rep_name ^ "_defined", @{thm typedef_Rep_defined} OF pcpo_thms'), []), - ((Abs_name ^ "_defined", @{thm typedef_Abs_defined} OF pcpo_thms'), []) + ([((Binding.name (Rep_name ^ "_strict"), @{thm typedef_Rep_strict} OF pcpo_thms'), []), + ((Binding.name (Abs_name ^ "_strict"), @{thm typedef_Abs_strict} OF pcpo_thms'), []), + ((Binding.name (Rep_name ^ "_strict_iff"), @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []), + ((Binding.name (Abs_name ^ "_strict_iff"), @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []), + ((Binding.name (Rep_name ^ "_defined"), @{thm typedef_Rep_defined} OF pcpo_thms'), []), + ((Binding.name (Abs_name ^ "_defined"), @{thm typedef_Abs_defined} OF pcpo_thms'), []) ]) |> snd |> Sign.parent_path