--- a/src/HOL/Tools/TFL/tfl.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Jan 21 16:47:04 2009 +0100
@@ -390,7 +390,7 @@
(wfrec $ map_types poly_tvars R)
$ functional
val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
- val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
+ val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
in (thy', def) end;
end;
@@ -549,7 +549,7 @@
val ([def0], theory) =
thy
|> PureThy.add_defs false
- [Thm.no_attributes (fid ^ "_def", defn)]
+ [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
val def = Thm.freezeT def0;
val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
else ()
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Jan 21 16:47:04 2009 +0100
@@ -238,7 +238,7 @@
(Sign.base_name name, reccomb_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))
@@ -262,7 +262,7 @@
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
- |> PureThy.add_thmss [(("recs", rec_thms), [])]
+ |> PureThy.add_thmss [((Binding.name "recs", rec_thms), [])]
||> Sign.parent_path
||> Theory.checkpoint
|-> (fn thms => pair (reccomb_names, Library.flat thms))
@@ -316,7 +316,7 @@
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
- val def = ((Sign.base_name name) ^ "_def",
+ val def = (Binding.name (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))) @
fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
--- a/src/HOL/Tools/datatype_aux.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Wed Jan 21 16:47:04 2009 +0100
@@ -76,7 +76,7 @@
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
- #> PureThy.add_thmss [((label, thms), atts)]
+ #> PureThy.add_thmss [((Binding.name label, thms), atts)]
#-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
@@ -85,7 +85,7 @@
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
- #> PureThy.add_thms [((label, thms), atts)]
+ #> PureThy.add_thms [((Binding.name label, thms), atts)]
#-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
--- a/src/HOL/Tools/datatype_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -196,13 +196,13 @@
fun add_rules simps case_thms rec_thms inject distinct
weak_case_congs cong_att =
- PureThy.add_thmss [(("simps", simps), []),
- (("", flat case_thms @
+ PureThy.add_thmss [((Binding.name "simps", simps), []),
+ ((Binding.empty, flat case_thms @
flat distinct @ rec_thms), [Simplifier.simp_add]),
- (("", rec_thms), [Code.add_default_eqn_attribute]),
- (("", flat inject), [iff_add]),
- (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
- (("", weak_case_congs), [cong_att])]
+ ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
+ ((Binding.empty, flat inject), [iff_add]),
+ ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
+ ((Binding.empty, weak_case_congs), [cong_att])]
#> snd;
@@ -213,15 +213,15 @@
val inducts = ProjectRule.projections (ProofContext.init thy) induction;
fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
- [(("", nth inducts index), [Induct.induct_type name]),
- (("", exhaustion), [Induct.cases_type name])];
+ [((Binding.empty, nth inducts index), [Induct.induct_type name]),
+ ((Binding.empty, exhaustion), [Induct.cases_type name])];
fun unnamed_rule i =
- (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
+ ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
in
thy |> PureThy.add_thms
(maps named_rules infos @
map unnamed_rule (length infos upto length inducts - 1)) |> snd
- |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
+ |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
end;
@@ -451,7 +451,7 @@
|> store_thmss "inject" new_type_names inject
||>> store_thmss "distinct" new_type_names distinct
||> Sign.add_path (space_implode "_" new_type_names)
- ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])];
+ ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
--- a/src/HOL/Tools/datatype_realizer.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Jan 21 16:47:04 2009 +0100
@@ -130,7 +130,7 @@
val vs = map (fn i => List.nth (pnames, i)) is;
val (thm', thy') = thy
|> Sign.absolute_path
- |> PureThy.store_thm (space_implode "_" (ind_name :: vs @ ["correctness"]), thm)
+ |> PureThy.store_thm (Binding.name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
@@ -196,7 +196,7 @@
val exh_name = Thm.get_name exhaustion;
val (thm', thy') = thy
|> Sign.absolute_path
- |> PureThy.store_thm (exh_name ^ "_P_correctness", thm)
+ |> PureThy.store_thm (Binding.name (exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Jan 21 16:47:04 2009 +0100
@@ -242,7 +242,7 @@
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], i + 1) end;
@@ -343,7 +343,7 @@
val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
val fTs = map fastype_of fs;
- val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
+ val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"),
Logic.mk_equals (Const (iso_name, T --> Univ_elT),
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') =
@@ -631,7 +631,7 @@
val ([dt_induct'], thy7) =
thy6
|> Sign.add_path big_name
- |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
+ |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
||> Sign.parent_path
||> Theory.checkpoint;
--- a/src/HOL/Tools/function_package/size.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Wed Jan 21 16:47:04 2009 +0100
@@ -144,7 +144,7 @@
(size_names ~~ recTs1))
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
- (def_names ~~ (size_fns ~~ rec_combs1)))
+ (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
||> TheoryTarget.instantiation
(map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
||>> fold_map define_overloaded
@@ -208,7 +208,7 @@
prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
val ([size_thms], thy'') = PureThy.add_thmss
- [(("size", size_eqns),
+ [((Binding.name "size", size_eqns),
[Simplifier.simp_add, Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
--- a/src/HOL/Tools/inductive_realizer.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Jan 21 16:47:04 2009 +0100
@@ -391,14 +391,14 @@
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
[K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
- val (thm', thy') = PureThy.store_thm (space_implode "_"
- (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
+ val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+ (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
(DatatypeAux.split_conj_thm thm');
val ([thms'], thy'') = PureThy.add_thmss
- [((space_implode "_"
+ [((Binding.name (space_implode "_"
(NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
- ["correctness"]), thms), [])] thy';
+ ["correctness"])), thms), [])] thy';
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
in
Extraction.add_realizers_i
@@ -451,8 +451,8 @@
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
- val (thm', thy') = PureThy.store_thm (space_implode "_"
- (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
+ val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
+ (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
in
Extraction.add_realizers_i
[mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
--- a/src/HOL/Tools/old_primrec_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -305,11 +305,11 @@
end;
fun thy_note ((name, atts), thms) =
- PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+ PureThy.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
fun thy_def false ((name, atts), t) =
- PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+ PureThy.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
| thy_def true ((name, atts), t) =
- PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+ PureThy.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
in
--- a/src/HOL/Tools/recdef_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/recdef_package.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Wrapper module for Konrad Slind's TFL package.
@@ -16,10 +15,10 @@
val cong_del: attribute
val wf_add: attribute
val wf_del: attribute
- val add_recdef: bool -> xstring -> string -> ((bstring * string) * Attrib.src list) list ->
+ val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
Attrib.src option -> theory -> theory
* {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
- val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * attribute list) list ->
+ val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
-> theory -> theory * {induct_rules: thm}
@@ -214,8 +213,8 @@
thy
|> Sign.add_path bname
|> PureThy.add_thmss
- ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
- ||>> PureThy.add_thms [(("induct", induct), [])];
+ (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+ ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
thy
@@ -243,7 +242,7 @@
val ([induct_rules'], thy3) =
thy2
|> Sign.add_path bname
- |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
+ |> PureThy.add_thms [((Binding.name "induct_rules", induct_rules), [])]
||> Sign.parent_path;
in (thy3, {induct_rules = induct_rules'}) end;
@@ -299,7 +298,7 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
+ P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
-- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
--- a/src/HOL/Tools/record_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -1534,8 +1534,10 @@
|> extension_typedef name repT (alphas@[zeta])
||> Sign.add_consts_i
(map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
- ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
- ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
+ ||>> PureThy.add_defs false
+ (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
+ ||>> PureThy.add_defs false
+ (map (Thm.no_attributes o apfst Binding.name) upd_specs)
|-> (fn args as ((_, dest_defs), upd_defs) =>
fold Code.add_default_eqn dest_defs
#> fold Code.add_default_eqn upd_defs
@@ -1693,14 +1695,14 @@
[dest_convs',upd_convs']),
thm_thy) =
defs_thy
- |> (PureThy.add_thms o map Thm.no_attributes)
+ |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
[("ext_inject", inject),
("ext_induct", induct),
("ext_cases", cases),
("ext_surjective", surjective),
("ext_split", split_meta)]
- ||>> (PureThy.add_thmss o map Thm.no_attributes)
- [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
+ ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
+ [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)]
in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
end;
@@ -1938,9 +1940,9 @@
(map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
|> (Sign.add_consts_i o map Syntax.no_syn)
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
- |> ((PureThy.add_defs false o map Thm.no_attributes) sel_specs)
- ||>> ((PureThy.add_defs false o map Thm.no_attributes) upd_specs)
- ||>> ((PureThy.add_defs false o map Thm.no_attributes)
+ |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
+ ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
+ ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
[make_spec, fields_spec, extend_spec, truncate_spec])
|-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
fold Code.add_default_eqn sel_defs
@@ -2164,17 +2166,17 @@
val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
[surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
defs_thy
- |> (PureThy.add_thmss o map Thm.no_attributes)
+ |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
[("select_convs", sel_convs_standard),
("update_convs", upd_convs),
("select_defs", sel_defs),
("update_defs", upd_defs),
("splits", [split_meta_standard,split_object,split_ex]),
("defs", derived_defs)]
- ||>> (PureThy.add_thms o map Thm.no_attributes)
+ ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
[("surjective", surjective),
("equality", equality)]
- ||>> PureThy.add_thms
+ ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
[(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
(("induct", induct), induct_type_global name),
(("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
@@ -2186,8 +2188,8 @@
val final_thy =
thms_thy
|> (snd oo PureThy.add_thmss)
- [(("simps", sel_upd_simps), [Simplifier.simp_add]),
- (("iffs",iffs), [iff_add])]
+ [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
+ ((Binding.name "iffs", iffs), [iff_add])]
|> put_record name (make_record_info args parent fields extension induct_scheme')
|> put_sel_upd (names @ [full_moreN]) sel_upd_simps
|> add_record_equalities extension_id equality'
--- a/src/HOL/Tools/res_axioms.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Wed Jan 21 16:47:04 2009 +0100
@@ -84,7 +84,7 @@
val (c, 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 thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
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 =
--- a/src/HOL/Tools/specification_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -28,7 +28,7 @@
else thname
val def_eq = Logic.mk_equals (Const(cname_full,ctype),
HOLogic.choice_const ctype $ P)
- val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
+ val (thms, thy') = PureThy.add_defs covld [((Binding.name cdefname, def_eq),[])] thy
val thm' = [thm,hd thms] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
@@ -39,7 +39,7 @@
let
fun process [] (thy,tm) =
let
- val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
+ val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
in
(thy',hd thms)
end
@@ -184,7 +184,7 @@
if name = ""
then arg |> Library.swap
else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm));
- PureThy.store_thm (name, thm) thy)
+ PureThy.store_thm (Binding.name name, thm) thy)
in
args |> apsnd (remove_alls frees)
|> apsnd undo_imps
--- a/src/HOL/Tools/typedef_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/typedef_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -112,7 +112,8 @@
if def then
theory
|> Sign.add_consts_i [(name, setT', NoSyn)]
- |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))]
+ |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
+ (PrimitiveDefs.mk_defpair (setC, set)))]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
fun contract_def NONE th = th
@@ -130,7 +131,7 @@
(Abs_name, oldT --> newT, NoSyn)]
#> add_def
#-> (fn set_def =>
- PureThy.add_axioms [((typedef_name, typedef_prop),
+ PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
[Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
##>> pair set_def)
##> Theory.add_deps "" (dest_Const RepC) typedef_deps
@@ -143,7 +144,7 @@
thy1
|> Sign.add_path name
|> PureThy.add_thms
- ([((Rep_name, make @{thm type_definition.Rep}), []),
+ ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
--- a/src/HOL/ex/Quickcheck.thy Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/ex/Quickcheck.thy Wed Jan 21 16:47:04 2009 +0100
@@ -200,7 +200,7 @@
in
lthy
|> LocalTheory.theory (Code.del_eqns c
- #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
#-> Code.add_eqn)
end;
in
--- a/src/Pure/Isar/calculation.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Jan 21 16:47:04 2009 +0100
@@ -98,8 +98,8 @@
("sym", sym_att, "declaration of symmetry rule"),
("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
PureThy.add_thms
- [(("", transitive_thm), [trans_add]),
- (("", symmetric_thm), [sym_add])] #> snd));
+ [((Binding.empty, transitive_thm), [trans_add]),
+ ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
--- a/src/Pure/Isar/constdefs.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Wed Jan 21 16:47:04 2009 +0100
@@ -8,12 +8,12 @@
signature CONSTDEFS =
sig
- val add_constdefs: (Binding.T * string option) list *
- ((Binding.T * string option * mixfix) option *
+ val add_constdefs: (binding * string option) list *
+ ((binding * string option * mixfix) option *
(Attrib.binding * string)) 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
+ val add_constdefs_i: (binding * typ option) list *
+ ((binding * typ option * mixfix) option *
+ ((binding * attribute list) * term)) list -> theory -> theory
end;
structure Constdefs: CONSTDEFS =
@@ -52,7 +52,7 @@
val thy' =
thy
|> Sign.add_consts_i [(c, T, mx)]
- |> PureThy.add_defs false [((name, def), atts)]
+ |> PureThy.add_defs false [((Binding.name name, def), atts)]
|-> (fn [thm] => Code.add_default_eqn thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/isar_cmd.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jan 21 16:47:04 2009 +0100
@@ -13,8 +13,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: ((Binding.T * string) * Attrib.src list) list -> theory -> theory
- val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory
+ val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
+ val add_defs: (bool * bool) * ((binding * 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
@@ -53,7 +53,6 @@
val print_theorems: Toplevel.transition -> Toplevel.transition
val print_locales: Toplevel.transition -> Toplevel.transition
val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
- val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
val print_attributes: Toplevel.transition -> Toplevel.transition
val print_simpset: Toplevel.transition -> Toplevel.transition
val print_rules: Toplevel.transition -> Toplevel.transition
@@ -359,12 +358,6 @@
Toplevel.keep (fn state =>
Locale.print_locale (Toplevel.theory_of state) show_facts name);
-fun print_registrations show_wits name = Toplevel.unknown_context o
- Toplevel.keep (Toplevel.node_case
- (Context.cases (Old_Locale.print_registrations show_wits name o ProofContext.init)
- (Old_Locale.print_registrations show_wits name))
- (Old_Locale.print_registrations show_wits name o Proof.context_of));
-
val print_attributes = Toplevel.unknown_theory o
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
--- a/src/Pure/Isar/overloading.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Jan 21 16:47:04 2009 +0100
@@ -134,8 +134,8 @@
fun declare c_ty = pair (Const c_ty);
-fun define checked name (c, t) =
- Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
+ Logic.mk_equals (Const (c, Term.fastype_of t), t));
(* target *)
--- a/src/Pure/ML/ml_context.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Jan 21 16:47:04 2009 +0100
@@ -126,7 +126,8 @@
fun ml_store sel (name, ths) =
let
- val ths' = Context.>>> (Context.map_theory_result (PureThy.store_thms (name, ths)));
+ val ths' = Context.>>> (Context.map_theory_result
+ (PureThy.store_thms (Binding.name name, ths)));
val _ =
if name = "" then ()
else if not (ML_Syntax.is_identifier name) then
--- a/src/Pure/Proof/extraction.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Jan 21 16:47:04 2009 +0100
@@ -733,11 +733,11 @@
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
|> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
- |> PureThy.add_defs false [((extr_name s vs ^ "_def",
+ |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
thy'
- |> PureThy.store_thm (corr_name s vs,
+ |> PureThy.store_thm (Binding.name (corr_name s vs),
Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
(Thm.forall_elim_var 0) (forall_intr_frees
(ProofChecker.thm_of_proof thy'
--- a/src/Pure/Tools/named_thms.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Tools/named_thms.ML
- ID: $Id$
Author: Makarius
Named collections of theorems in canonical order.
@@ -36,6 +35,6 @@
val setup =
Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
- PureThy.add_thms_dynamic (name, Data.get);
+ PureThy.add_thms_dynamic (Binding.name name, Data.get);
end;
--- a/src/Pure/assumption.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/assumption.ML Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/assumption.ML
- ID: $Id$
Author: Makarius
Local assumptions, parameterized by export rules.
@@ -79,7 +78,7 @@
(* named prems -- legacy feature *)
val _ = Context.>>
- (Context.map_theory (PureThy.add_thms_dynamic ("prems",
+ (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
--- a/src/Pure/axclass.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/axclass.ML Wed Jan 21 16:47:04 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/axclass.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Type classes defined as predicates, associated with a record of
@@ -9,7 +8,7 @@
signature AX_CLASS =
sig
val define_class: bstring * class list -> string list ->
- ((Binding.T * attribute list) * term list) list -> theory -> class * theory
+ ((binding * 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
@@ -329,7 +328,8 @@
quote (Syntax.string_of_classrel ctxt [c1, c2]));
in
thy
- |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
+ |> PureThy.add_thms [((Binding.name
+ (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
|-> (fn [th'] => add_classrel th')
end;
@@ -345,7 +345,7 @@
quote (Syntax.string_of_arity ctxt arity));
in
thy
- |> PureThy.add_thms (map (rpair []) (names ~~ ths))
+ |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
|-> fold add_arity
end;
@@ -372,10 +372,10 @@
|> Sign.no_base_names
|> 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'))
+ (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
#> snd
#> Sign.restore_naming thy
#> pair (Const (c, T))))
@@ -391,7 +391,7 @@
(NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
in
thy
- |> Thm.add_def false false (name', prop)
+ |> Thm.add_def false false (Binding.name name', prop)
|>> (fn thm => Drule.transitive_thm OF [eq, thm])
end;
@@ -469,7 +469,7 @@
val ([def], def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
+ |> PureThy.add_defs false [((Binding.name (Thm.def_name bconst), class_eq), [])];
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
@@ -515,7 +515,11 @@
val args = prep thy raw_args;
val specs = mk args;
val names = name args;
- in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
+ in
+ thy
+ |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
+ |-> fold add
+ end;
fun ax_classrel prep =
axiomatize (map o prep) (map Logic.mk_classrel)
--- a/src/Pure/drule.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/drule.ML Wed Jan 21 16:47:04 2009 +0100
@@ -460,10 +460,10 @@
val read_prop = certify o SimpleSyntax.read_prop;
fun store_thm name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm (name, th)));
+ Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
fun store_thm_open name th =
- Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
+ Context.>>> (Context.map_theory_result (PureThy.store_thm_open (Binding.name name, th)));
fun store_standard_thm name th = store_thm name (standard th);
fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
--- a/src/Pure/more_thm.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/more_thm.ML Wed Jan 21 16:47:04 2009 +0100
@@ -38,8 +38,8 @@
val forall_elim_vars: int -> thm -> thm
val unvarify: thm -> thm
val close_derivation: thm -> thm
- val add_axiom: bstring * term -> theory -> thm * theory
- val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
+ val add_axiom: binding * term -> theory -> thm * theory
+ val add_def: bool -> bool -> binding * term -> theory -> thm * theory
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
val theory_attributes: attribute list -> theory * thm -> theory * thm
@@ -276,14 +276,15 @@
(** specification primitives **)
-fun add_axiom (name, prop) thy =
+fun add_axiom (b, prop) thy =
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_bname thy' name'));
+ val b' = if Binding.is_empty b
+ then Binding.name ("axiom_" ^ serial_string ()) else b;
+ val thy' = thy |> Theory.add_axioms_i [(b', prop)];
+ val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' b'));
in (axm, thy') end;
-fun add_def unchecked overloaded (name, prop) thy =
+fun add_def unchecked overloaded (b, prop) thy =
let
val tfrees = rev (map TFree (Term.add_tfrees prop []));
val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
@@ -291,8 +292,8 @@
val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
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_bname thy' name);
+ val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
+ val axm' = Thm.axiom thy' (Sign.full_name thy' b);
val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
in (thm, thy') end;
--- a/src/Pure/pure_thy.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/pure_thy.ML Wed Jan 21 16:47:04 2009 +0100
@@ -24,27 +24,27 @@
val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
- val store_thms: bstring * thm list -> theory -> thm list * theory
- val store_thm: bstring * thm -> theory -> thm * theory
- val store_thm_open: bstring * thm -> theory -> thm * theory
- val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
- 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 -> ((Binding.T * attribute list) *
+ val store_thms: binding * thm list -> theory -> thm list * theory
+ val store_thm: binding * thm -> theory -> thm * theory
+ val store_thm_open: binding * thm -> theory -> thm * theory
+ val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory
+ val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
+ val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
+ val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
+ val note_thmss: string -> ((binding * attribute list) *
(thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
- val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) *
+ val note_thmss_grouped: string -> string -> ((binding * 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: ((binding * term) * attribute list) list -> theory -> thm list * theory
val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
- val add_defs: bool -> ((bstring * term) * attribute list) list ->
+ val add_defs: bool -> ((binding * term) * attribute list) list ->
theory -> thm list * theory
- val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
+ val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
+ theory -> thm list * theory
+ val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
theory -> thm list * theory
val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
theory -> thm list * theory
- val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
- theory -> thm list * theory
val old_appl_syntax: theory -> bool
val old_appl_syntax_setup: theory -> theory
end;
@@ -163,21 +163,21 @@
(* store_thm(s) *)
-fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
- (name_thms false true Position.none) I (Binding.name bname, thms);
+fun store_thms (b, thms) = enter_thms (name_thms true true Position.none)
+ (name_thms false true Position.none) I (b, thms);
-fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
+fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
-fun store_thm_open (bname, th) =
+fun store_thm_open (b, th) =
enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
- (Binding.name bname, [th]) #>> the_single;
+ (b, [th]) #>> the_single;
(* add_thms(s) *)
-fun add_thms_atts pre_name ((bname, thms), atts) =
+fun add_thms_atts pre_name ((b, thms), atts) =
enter_thms pre_name (name_thms false true Position.none)
- (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms);
+ (foldl_map (Thm.theory_attributes atts)) (b, thms);
fun gen_add_thmss pre_name =
fold_map (add_thms_atts pre_name);
@@ -192,9 +192,9 @@
(* add_thms_dynamic *)
-fun add_thms_dynamic (bname, f) thy = thy
+fun add_thms_dynamic (b, f) thy = thy
|> (FactsData.map o apfst)
- (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd);
+ (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
(* note_thmss *)
@@ -224,21 +224,21 @@
(* store axioms as theorems *)
local
- fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name);
+ fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
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 =>
+ fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy =>
let
- val named_ax = [(name, ax)];
+ val named_ax = [(b, ax)];
val thy' = add named_ax thy;
- val thm = hd (get_axs thy' named_ax);
- in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
+ val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax));
+ in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end);
in
- val add_defs = add_axm o Theory.add_defs_i false;
- val add_defs_unchecked = add_axm o Theory.add_defs_i true;
- val add_axioms = add_axm Theory.add_axioms_i;
- val add_defs_cmd = add_axm o Theory.add_defs false;
- val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
- val add_axioms_cmd = add_axm Theory.add_axioms;
+ val add_defs = add_axm I o Theory.add_defs_i false;
+ val add_defs_unchecked = add_axm I o Theory.add_defs_i true;
+ val add_axioms = add_axm I Theory.add_axioms_i;
+ val add_defs_cmd = add_axm Binding.name o Theory.add_defs false;
+ val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true;
+ val add_axioms_cmd = add_axm Binding.name Theory.add_axioms;
end;
@@ -378,16 +378,16 @@
("sort_constraint", typ "'a itself => prop", NoSyn),
("conjunction", typ "prop => prop => prop", NoSyn)]
#> (add_defs false o map Thm.no_attributes)
- [("prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
- ("term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
- ("sort_constraint_def",
+ [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
+ (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
+ (Binding.name "sort_constraint_def",
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
- ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+ (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
#> Sign.hide_const false "Pure.term"
#> Sign.hide_const false "Pure.sort_constraint"
#> Sign.hide_const false "Pure.conjunction"
- #> add_thmss [(("nothing", []), [])] #> snd
- #> Theory.add_axioms_i Proofterm.equality_axms));
+ #> add_thmss [((Binding.name "nothing", []), [])] #> snd
+ #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms)));
end;
--- a/src/ZF/Tools/datatype_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -247,7 +247,7 @@
if need_recursor then
thy |> Sign.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
+ |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
else thy;
val (con_defs, thy0) = thy_path
@@ -255,7 +255,7 @@
((case_base_name, case_typ, NoSyn) ::
map #1 (List.concat con_ty_lists))
|> PureThy.add_defs false
- (map Thm.no_attributes
+ (map (Thm.no_attributes o apfst Binding.name)
(case_def ::
List.concat (ListPair.map mk_con_defs
(1 upto npart, con_ty_lists))))
@@ -383,13 +383,13 @@
(*Updating theory components: simprules and datatype info*)
(thy1 |> Sign.add_path big_rec_base_name
|> PureThy.add_thmss
- [(("simps", simps), [Simplifier.simp_add]),
- (("", intrs), [Classical.safe_intro NONE]),
- (("con_defs", con_defs), []),
- (("case_eqns", case_eqns), []),
- (("recursor_eqns", recursor_eqns), []),
- (("free_iffs", free_iffs), []),
- (("free_elims", free_SEs), [])] |> snd
+ [((Binding.name "simps", simps), [Simplifier.simp_add]),
+ ((Binding.empty , intrs), [Classical.safe_intro NONE]),
+ ((Binding.name "con_defs", con_defs), []),
+ ((Binding.name "case_eqns", case_eqns), []),
+ ((Binding.name "recursor_eqns", recursor_eqns), []),
+ ((Binding.name "free_iffs", free_iffs), []),
+ ((Binding.name "free_elims", free_SEs), [])] |> snd
|> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
|> ConstructorsData.map (fold Symtab.update con_pairs)
|> Sign.parent_path,
--- a/src/ZF/Tools/induct_tacs.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Wed Jan 21 16:47:04 2009 +0100
@@ -158,7 +158,7 @@
in
thy
|> Sign.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
+ |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
|> Sign.parent_path
--- a/src/ZF/Tools/inductive_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -27,10 +27,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 ->
- ((Binding.T * term) * attribute list) list ->
+ ((binding * term) * attribute list) list ->
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
- ((Binding.T * string) * Attrib.src list) list ->
+ ((binding * 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
@@ -173,7 +173,7 @@
val (_, thy1) =
thy
|> Sign.add_path big_rec_base_name
- |> PureThy.add_defs false (map Thm.no_attributes axpairs);
+ |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
val ctxt1 = ProofContext.init thy1;
@@ -510,9 +510,9 @@
val ([induct', mutual_induct'], thy') =
thy
- |> PureThy.add_thms [((co_prefix ^ "induct", induct),
+ |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
[case_names, Induct.induct_pred big_rec_name]),
- (("mutual_induct", mutual_induct), [case_names])];
+ ((Binding.name "mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
end; (*of induction_rules*)
@@ -522,7 +522,7 @@
if not coind then induction_rules raw_induct thy1
else
(thy1
- |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])]
+ |> PureThy.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
|> apfst hd |> Library.swap, TrueI)
and defs = big_rec_def :: part_rec_defs
@@ -531,15 +531,15 @@
thy2
|> IndCases.declare big_rec_name make_cases
|> PureThy.add_thms
- [(("bnd_mono", bnd_mono), []),
- (("dom_subset", dom_subset), []),
- (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
+ [((Binding.name "bnd_mono", bnd_mono), []),
+ ((Binding.name "dom_subset", dom_subset), []),
+ ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
- [("defs", defs),
- ("intros", intrs)];
+ [(Binding.name "defs", defs),
+ (Binding.name "intros", intrs)];
val (intrs'', thy4) =
thy3
- |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
+ |> PureThy.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
||> Sign.parent_path;
in
(thy4,
--- a/src/ZF/Tools/primrec_package.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML Wed Jan 21 16:47:04 2009 +0100
@@ -8,8 +8,8 @@
signature PRIMREC_PACKAGE =
sig
- 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
+ val add_primrec: ((binding * string) * Attrib.src list) list -> theory -> theory * thm list
+ val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -169,7 +169,7 @@
val ([def_thm], thy1) = thy
|> Sign.add_path (Sign.base_name fname)
- |> (PureThy.add_defs false o map Thm.no_attributes) [def];
+ |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val eqn_thms =
@@ -179,10 +179,10 @@
val (eqn_thms', thy2) =
thy1
- |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
+ |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
- |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
+ |> PureThy.add_thmss [((Binding.name "simps", eqn_thms'), [Simplifier.simp_add])]
||> Sign.parent_path;
in (thy3, eqn_thms') end;