--- 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;
--- 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
--- 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 =
--- 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 <ak1> ... <akn> *)
@@ -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_<ak>_inst: *)
(* at TYPE(<ak>) *)
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_<ak>_inst: *)
(* pt TYPE('x::pt_<ak>) TYPE(<ak>) *)
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_<ak>_inst: *)
(* fs TYPE('x::pt_<ak>) TYPE (<ak>) *)
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
--- 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;
--- 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))
--- 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);
--- 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;
--- 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 *)
--- 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;
--- 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 ),
--- 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;
--- 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