--- a/TFL/tfl.sml Tue Jan 12 13:40:08 1999 +0100
+++ b/TFL/tfl.sml Tue Jan 12 13:54:51 1999 +0100
@@ -339,7 +339,7 @@
Sign.infer_types (sign_of thy) (K None) (K None) [] false
([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M],
propT)
- in PureThy.add_defs_i [Attribute.none (def_name, def_term)] thy end
+ in PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy end
end;
@@ -461,7 +461,7 @@
val R'abs = S.rand R'
val theory =
thy
- |> PureThy.add_defs_i [Attribute.none (Name ^ "_def", subst_free[(R1,R')] proto_def)];
+ |> PureThy.add_defs_i [Thm.no_attributes (Name ^ "_def", subst_free[(R1,R')] proto_def)];
val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
val fconst = #lhs(S.dest_eq(concl def))
val tych = Thry.typecheck theory
--- a/src/HOL/HOL.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/HOL.ML Tue Jan 12 13:54:51 1999 +0100
@@ -422,7 +422,7 @@
local
-fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x;
+fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
in
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 12 13:54:51 1999 +0100
@@ -275,7 +275,7 @@
in
(thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_tthmss [(("recs", Attribute.tthms_of rec_thms), [])] |>
+ PureThy.add_thmss [(("recs", rec_thms), [])] |>
Theory.parent_path,
reccomb_names, rec_thms)
end;
@@ -518,7 +518,7 @@
in
(thy' |> Theory.add_path big_name |>
- PureThy.add_tthmss [(("size", Attribute.tthms_of size_thms), [])] |>
+ PureThy.add_thmss [(("size", size_thms), [])] |>
Theory.parent_path,
size_thms)
end;
--- a/src/HOL/Tools/datatype_aux.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Tue Jan 12 13:54:51 1999 +0100
@@ -78,14 +78,14 @@
fun store_thmss label tnames thmss thy =
foldr (fn ((tname, thms), thy') => thy' |>
Theory.add_path tname |>
- PureThy.add_tthmss [((label, Attribute.tthms_of thms), [])] |>
+ PureThy.add_thmss [((label, thms), [])] |>
Theory.parent_path)
(tnames ~~ thmss, thy);
fun store_thms label tnames thms thy =
foldr (fn ((tname, thm), thy') => thy' |>
Theory.add_path tname |>
- PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
+ PureThy.add_thms [((label, thm), [])] |>
Theory.parent_path)
(tnames ~~ thms, thy);
--- a/src/HOL/Tools/datatype_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -402,7 +402,7 @@
val thy11 = thy10 |>
Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+ PureThy.add_thmss [(("simps", simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
Theory.parent_path;
@@ -459,7 +459,7 @@
val thy11 = thy10 |>
Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+ PureThy.add_thmss [(("simps", simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
Theory.parent_path;
@@ -550,7 +550,7 @@
val thy9 = thy8 |>
Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+ PureThy.add_thmss [(("simps", simps), [])] |>
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
Theory.parent_path;
@@ -571,8 +571,7 @@
simps = simps})
end;
-val rep_datatype = gen_rep_datatype
- (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm;
+val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm;
val rep_datatype_i = gen_rep_datatype (K I) (K I);
(******************************** add datatype ********************************)
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 12 13:54:51 1999 +0100
@@ -535,7 +535,7 @@
val thy7 = thy6 |>
Theory.add_path big_name |>
- PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |>
+ PureThy.add_thms [(("induct", dt_induct), [])] |>
Theory.parent_path;
in (thy7, constr_inject, dist_rewrites, dt_induct)
--- a/src/HOL/Tools/inductive_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -464,12 +464,11 @@
else standard (raw_induct RSN (2, rev_mp));
val thy'' = thy' |>
- PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
- (if no_elim then I else PureThy.add_tthmss
- [(("elims", Attribute.tthms_of elims), [])]) |>
- (if no_ind then I else PureThy.add_tthms
- [(((if coind then "co" else "") ^ "induct",
- Attribute.tthm_of induct), [])]) |>
+ PureThy.add_thmss [(("intrs", intrs), [])] |>
+ (if no_elim then I else PureThy.add_thmss
+ [(("elims", elims), [])]) |>
+ (if no_ind then I else PureThy.add_thms
+ [(((if coind then "co" else "") ^ "induct", induct), [])]) |>
Theory.parent_path;
in (thy'',
@@ -517,7 +516,7 @@
val thy'' = thy' |>
(if coind then I
- else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
+ else PureThy.add_thms [(("induct", induct), [])]) |>
Theory.parent_path
in (thy'',
@@ -600,8 +599,8 @@
val intr_ts'' = map subst intr_ts';
in add_inductive_i verbose false "" coind false false cs'' intr_ts''
- (Attribute.thms_of (PureThy.get_tthmss thy monos))
- (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
+ (PureThy.get_thmss thy monos)
+ (PureThy.get_thmss thy con_defs) thy
end;
end;
--- a/src/HOL/Tools/primrec_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/primrec_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -235,11 +235,11 @@
commas names1 ^ " ...");
val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
(fn _ => [rtac refl 1])) eqns;
- val tsimps = Attribute.tthms_of char_thms;
+ val simps = char_thms;
val thy'' = thy' |>
- PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |>
- PureThy.add_tthms (map (rpair [])
- (filter_out (equal "" o fst) (map fst eqns ~~ tsimps))) |>
+ PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |>
+ PureThy.add_thms (map (rpair [])
+ (filter_out (equal "" o fst) (map fst eqns ~~ simps))) |>
Theory.parent_path;
in
(thy'', char_thms)
--- a/src/HOL/Tools/record_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/record_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -53,7 +53,7 @@
let
val ss = Simplifier.simpset_ref_of thy;
val cs = Classical.claset_ref_of thy;
- val (cs', ss') = (! cs, ! ss) addIffs [Attribute.thm_of th];
+ val (cs', ss') = (! cs, ! ss) addIffs [th];
in ss := ss'; cs := cs'; (thy, th) end;
fun add_wrapper wrapper thy =
@@ -68,7 +68,7 @@
val (op :==) = Logic.mk_defpair;
val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs;
+fun get_defs thy specs = map (PureThy.get_thm thy o fst) specs;
(* proof by simplification *)
@@ -76,14 +76,13 @@
fun prove_simp thy tacs simps =
let
val sign = Theory.sign_of thy;
- val ss = Simplifier.addsimps (HOL_basic_ss, Attribute.thms_of simps);
+ val ss = Simplifier.addsimps (HOL_basic_ss, simps);
fun prove goal =
- Attribute.tthm_of
- (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
- (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)]))
- handle ERROR => error ("The error(s) above occurred while trying to prove "
- ^ quote (Sign.string_of_term sign goal)));
+ Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
+ (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)]))
+ handle ERROR => error ("The error(s) above occurred while trying to prove "
+ ^ quote (Sign.string_of_term sign goal));
in prove end;
@@ -328,12 +327,12 @@
{args: (string * sort) list,
parent: (typ list * string) option,
fields: (string * typ) list,
- simps: tthm list};
+ simps: thm list};
type parent_info =
{name: string,
fields: (string * typ) list,
- simps: tthm list};
+ simps: thm list};
(* data kind 'HOL/records' *)
@@ -519,12 +518,10 @@
(* 1st stage: types_thy *)
- val (types_thy, simps) =
+ val (types_thy, datatype_simps) =
thy
|> field_type_defs fieldT_specs;
- val datatype_simps = Attribute.tthms_of simps;
-
(* 2nd stage: defs_thy *)
@@ -532,7 +529,7 @@
types_thy
|> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
(field_decls @ dest_decls)
- |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
+ |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
(field_specs @ dest_specs);
val field_defs = get_defs defs_thy field_specs;
@@ -547,14 +544,14 @@
val field_injects = map prove_std inject_props;
val dest_convs = map prove_std dest_props;
val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1]
- (map (apfst Thm.symmetric) field_defs @ dest_convs)) surj_props;
+ (map Thm.symmetric field_defs @ dest_convs)) surj_props;
fun mk_split th = SplitPairedAll.rule (th RS eq_reflection);
- val field_splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs;
+ val field_splits = map mk_split surj_pairs;
val thms_thy =
defs_thy
- |> (PureThy.add_tthmss o map Attribute.none)
+ |> (PureThy.add_thmss o map Thm.no_attributes)
[("field_defs", field_defs),
("dest_defs", dest_defs),
("dest_convs", dest_convs),
@@ -692,7 +689,7 @@
|> Theory.add_path bname
|> field_definitions fields names zeta moreT more vars named_vars;
- val named_splits = map2 (fn (c, (th, _)) => (suffix field_typeN c, th)) (names, field_splits);
+ val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits);
(* 2nd stage: defs_thy *)
@@ -705,9 +702,9 @@
|> Theory.add_trfuns ([], [], field_tr's, [])
|> (Theory.add_consts_i o map Syntax.no_syn)
(sel_decls @ update_decls @ make_decls)
- |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
+ |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
(sel_specs @ update_specs)
- |> (PureThy.add_defs_i o map Attribute.none) make_specs;
+ |> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
val sel_defs = get_defs defs_thy sel_specs;
val update_defs = get_defs defs_thy update_specs;
@@ -726,13 +723,13 @@
val thms_thy =
defs_thy
- |> (PureThy.add_tthmss o map Attribute.none)
+ |> (PureThy.add_thmss o map Thm.no_attributes)
[("select_defs", sel_defs),
("update_defs", update_defs),
("make_defs", make_defs),
("select_convs", sel_convs),
("update_convs", update_convs)]
- |> PureThy.add_tthmss
+ |> PureThy.add_thmss
[(("simps", simps), [Simplifier.simp_add_global]),
(("iffs", field_injects), [add_iffs_global])];
--- a/src/HOL/Tools/typedef_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/typedef_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -141,9 +141,9 @@
((if no_def then [] else [(name, setT, NoSyn)]) @
[(Rep_name, newT --> oldT, NoSyn),
(Abs_name, oldT --> newT, NoSyn)])
- |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none)
+ |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
[(name ^ "_def", Logic.mk_equals (setC, set))])
- |> (PureThy.add_axioms_i o map Attribute.none)
+ |> (PureThy.add_axioms_i o map Thm.no_attributes)
[(Rep_name, rep_type),
(Rep_name ^ "_inverse", rep_type_inv),
(Abs_name ^ "_inverse", abs_type_inv)]
--- a/src/HOLCF/domain/axioms.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOLCF/domain/axioms.ML Tue Jan 12 13:54:51 1999 +0100
@@ -86,7 +86,7 @@
[take_def, finite_def])
end; (* let *)
-val add_axioms_i = PureThy.add_axioms_i o map Attribute.none;
+val add_axioms_i = PureThy.add_axioms_i o map Thm.no_attributes;
in (* local *)
--- a/src/HOLCF/domain/theorems.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOLCF/domain/theorems.ML Tue Jan 12 13:54:51 1999 +0100
@@ -323,7 +323,7 @@
(filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
val copy_rews = copy_strict::copy_apps @ copy_stricts;
in thy |> Theory.add_path (Sign.base_name dname)
- |> (PureThy.add_tthmss o map Attribute.no_attrss) [
+ |> (PureThy.add_thmss o map Thm.no_attributes) [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
("casedist" , [casedist]),
@@ -598,7 +598,7 @@
in thy |> Theory.add_path comp_dnam
- |> (PureThy.add_tthmss o map Attribute.no_attrss) [
+ |> (PureThy.add_thmss o map Thm.no_attributes) [
("take_rews" , take_rews ),
("take_lemmas", take_lemmas),
("finites" , finites ),
--- a/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -245,7 +245,7 @@
if need_recursor then
thy |> Theory.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> PureThy.add_defs_i [Attribute.none recursor_def]
+ |> PureThy.add_defs_i [Thm.no_attributes recursor_def]
else thy;
val thy0 = thy_path
@@ -253,7 +253,7 @@
((case_base_name, case_typ, NoSyn) ::
map #1 (flat con_ty_lists))
|> PureThy.add_defs_i
- (map Attribute.none
+ (map Thm.no_attributes
(case_def ::
flat (ListPair.map mk_con_defs
(1 upto npart, con_ty_lists))))
@@ -392,8 +392,7 @@
in
(*Updating theory components: simprules and datatype info*)
(thy1 |> Theory.add_path big_rec_base_name
- |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps),
- [Simplifier.simp_add_global])]
+ |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
|> DatatypesData.put
(Symtab.update
((big_rec_name, dt_info), DatatypesData.get thy1))
--- a/src/ZF/Tools/induct_tacs.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Tue Jan 12 13:54:51 1999 +0100
@@ -165,8 +165,7 @@
in
thy |> Theory.add_path (Sign.base_name big_rec_name)
- |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps),
- [Simplifier.simp_add_global])]
+ |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
|> DatatypesData.put
(Symtab.update
((big_rec_name, dt_info), DatatypesData.get thy))
--- a/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -169,7 +169,7 @@
(*add definitions of the inductive sets*)
val thy1 = thy |> Theory.add_path big_rec_base_name
- |> PureThy.add_defs_i (map Attribute.none axpairs)
+ |> PureThy.add_defs_i (map Thm.no_attributes axpairs)
(*fetch fp definitions from the theory*)
@@ -519,9 +519,9 @@
and mutual_induct = CP.remove_split mutual_induct_fsplit
in
(thy
- |> PureThy.add_tthms
- [(("induct", Attribute.tthm_of induct), []),
- (("mutual_induct", Attribute.tthm_of mutual_induct), [])],
+ |> PureThy.add_thms
+ [(("induct", induct), []),
+ (("mutual_induct", mutual_induct), [])],
induct, mutual_induct)
end; (*of induction_rules*)
@@ -534,13 +534,13 @@
in
(thy2
- |> PureThy.add_tthms
- [(("bnd_mono", Attribute.tthm_of bnd_mono), []),
- (("dom_subset", Attribute.tthm_of dom_subset), []),
- (("elim", Attribute.tthm_of elim), [])]
- |> PureThy.add_tthmss
- [(("defs", Attribute.tthms_of defs), []),
- (("intrs", Attribute.tthms_of intrs), [])]
+ |> (PureThy.add_thms o map Thm.no_attributes)
+ [("bnd_mono", bnd_mono),
+ ("dom_subset", dom_subset),
+ ("elim", elim)]
+ |> (PureThy.add_thmss o map Thm.no_attributes)
+ [("defs", defs),
+ ("intrs", intrs)]
|> Theory.parent_path,
{defs = defs,
bnd_mono = bnd_mono,
--- a/src/ZF/Tools/primrec_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/ZF/Tools/primrec_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -173,20 +173,20 @@
val rewrites = get_axiom thy' (#1 def) ::
map mk_meta_eq (#rec_rewrites con_info)
val char_thms =
- (if !Ind_Syntax.trace then
+ (if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *)
writeln ("Proving equations for primrec function " ^ fname)
else ();
- map (fn (_,t) =>
+ map (fn (_,t) =>
prove_goalw_cterm rewrites
(Ind_Syntax.traceIt "next primrec equation = "
(cterm_of (sign_of thy') t))
(fn _ => [rtac refl 1]))
recursion_eqns);
- val tsimps = Attribute.tthms_of char_thms;
+ val simps = char_thms;
val thy'' = thy'
- |> PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])]
- |> PureThy.add_tthms (map (rpair [])
- (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ tsimps)))
+ |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
+ |> PureThy.add_thms (map (rpair [])
+ (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps)))
|> Theory.parent_path;
in
(thy'', char_thms)