--- a/src/HOL/Import/proof_kernel.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Jul 29 08:15:40 2008 +0200
@@ -1932,7 +1932,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_i false [((thmname,eq),[])] thy1
+ val (thms, thy2) = PureThy.add_defs false [((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 Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Import/replay.ML Tue Jul 29 08:15:40 2008 +0200
@@ -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_i false [((thmname, eq), [])] thy)
+ snd (PureThy.add_defs false [((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 Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jul 29 08:15:40 2008 +0200
@@ -152,7 +152,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_i true [((name, def2),[])]
+ |> PureThy.add_defs_unchecked true [((name, def2),[])]
|> snd
|> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
end) ak_names_types thy1;
@@ -207,7 +207,7 @@
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_i true [((name, def),[])] thy'
+ PureThy.add_defs_unchecked true [((name, def),[])] thy'
end) ak_names_types thy) ak_names_types thy4;
(* proves that every atom-kind is an instance of at *)
--- a/src/HOL/Nominal/nominal_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -617,7 +617,7 @@
val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
val T = Type (Sign.intern_type thy name, tvs');
in apfst (pair r o hd)
- (PureThy.add_defs_unchecked_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
+ (PureThy.add_defs_unchecked true [(("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 $
@@ -783,7 +783,7 @@
val def_name = (Sign.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
Sign.add_consts_i [(cname', constrT, mx)] |>
- (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
+ (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)]
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
@@ -1965,7 +1965,7 @@
|> Sign.add_consts_i (map (fn ((name, T), T') =>
(Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
- |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+ |> (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,
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Jul 29 08:15:40 2008 +0200
@@ -391,9 +391,9 @@
fun thy_note ((name, atts), thms) =
PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
fun thy_def false ((name, atts), t) =
- PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+ PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
| thy_def true ((name, atts), t) =
- PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+ PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
in
--- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Jul 29 08:15:40 2008 +0200
@@ -671,7 +671,7 @@
setup {*
Theory.add_consts_i const_decls
-#> (fn thy => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy
+#> (fn thy => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
in (da := thm; thy') end)
*}
--- a/src/HOL/Tools/TFL/tfl.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Jul 29 08:15:40 2008 +0200
@@ -392,7 +392,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_i false [Thm.no_attributes (def_name, def_term)] thy
+ val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
in (thy', def) end;
end;
@@ -550,7 +550,7 @@
val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
val ([def0], theory) =
thy
- |> PureThy.add_defs_i false
+ |> PureThy.add_defs false
[Thm.no_attributes (fid ^ "_def", defn)]
val def = Thm.freezeT def0;
val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Jul 29 08:15:40 2008 +0200
@@ -239,7 +239,7 @@
|> Sign.add_consts_i (map (fn ((name, T), T') =>
(Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
- |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
+ |> (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,
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
@@ -323,7 +323,7 @@
val ([def_thm], thy') =
thy
|> Sign.declare_const [] decl |> snd
- |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
+ |> (PureThy.add_defs false o map Thm.no_attributes) [def];
in (defs @ [def_thm], thy')
end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jul 29 08:15:40 2008 +0200
@@ -244,7 +244,7 @@
val ([def_thm], thy') =
thy
|> Sign.add_consts_i [(cname', constrT, mx)]
- |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
+ |> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
@@ -348,7 +348,7 @@
val defs = map (fn (rec_name, (T, iso_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') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
+ val (def_thms, thy') = (PureThy.add_defs false o map Thm.no_attributes) defs thy;
(* prove characteristic equations *)
--- a/src/HOL/Tools/function_package/size.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML Tue Jul 29 08:15:40 2008 +0200
@@ -143,7 +143,7 @@
|> Sign.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
(size_names ~~ recTs1))
- |> PureThy.add_defs_i false
+ |> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
(def_names ~~ (size_fns ~~ rec_combs1)))
||> TheoryTarget.instantiation
--- a/src/HOL/Tools/old_primrec_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/old_primrec_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -308,9 +308,9 @@
fun thy_note ((name, atts), thms) =
PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
fun thy_def false ((name, atts), t) =
- PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
+ PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
| thy_def true ((name, atts), t) =
- PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
+ PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
in
--- a/src/HOL/Tools/record_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -1540,8 +1540,8 @@
|> 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_i false (map Thm.no_attributes (ext_spec::dest_specs))
- ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
+ ||>> PureThy.add_defs false (map Thm.no_attributes (ext_spec::dest_specs))
+ ||>> PureThy.add_defs false (map Thm.no_attributes upd_specs)
|-> (fn args as ((_, dest_defs), upd_defs) =>
fold Code.add_default_func dest_defs
#> fold Code.add_default_func upd_defs
@@ -1944,9 +1944,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_i false o map Thm.no_attributes) sel_specs)
- ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
- ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
+ |> ((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)
[make_spec, fields_spec, extend_spec, truncate_spec])
|-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
fold Code.add_default_func sel_defs
--- a/src/HOL/Tools/specification_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/specification_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -29,7 +29,7 @@
else thname
val def_eq = Logic.mk_equals (Const(cname_full,ctype),
HOLogic.choice_const ctype $ P)
- val (thms, thy') = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
+ val (thms, thy') = PureThy.add_defs covld [((cdefname,def_eq),[])] thy
val thm' = [thm,hd thms] MRS @{thm exE_some}
in
mk_definitional cos (thy',thm')
@@ -40,7 +40,7 @@
let
fun process [] (thy,tm) =
let
- val (thms, thy') = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
+ val (thms, thy') = PureThy.add_axioms [((axname,HOLogic.mk_Trueprop tm),[])] thy
in
(thy',hd thms)
end
--- a/src/HOL/Tools/typedef_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/typedef_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -128,7 +128,7 @@
fun add_def eq thy =
if def then
thy
- |> PureThy.add_defs_i false [Thm.no_attributes eq]
+ |> PureThy.add_defs false [Thm.no_attributes eq]
|-> (fn [th] => pair (SOME th))
else (NONE, thy);
@@ -140,7 +140,7 @@
[(Rep_name, newT --> oldT, NoSyn),
(Abs_name, oldT --> newT, NoSyn)])
#> add_def (PrimitiveDefs.mk_defpair (setC, set))
- ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
+ ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
[apsnd (fn cond_axm => nonempty RS cond_axm)])]
##> Theory.add_deps "" (dest_Const RepC) typedef_deps
##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -350,7 +350,7 @@
(automaton_name ^ "_trans",
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
[(automaton_name ^ "_initial_def",
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
(automaton_name ^ "_asig_def",
@@ -391,7 +391,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == " ^ comp_list)]
end)
@@ -406,7 +406,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
end)
@@ -420,7 +420,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
end)
@@ -446,7 +446,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
+|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
end)
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Tue Jul 29 08:15:40 2008 +0200
@@ -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_i (map Thm.no_attributes x);
+fun add_axioms_i x = snd o PureThy.add_axioms (map Thm.no_attributes 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_i false) (map Thm.no_attributes x);
+fun add_defs_i x = snd o (PureThy.add_defs false) (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
in (* local *)
--- a/src/HOLCF/Tools/fixrec_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -97,7 +97,7 @@
val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
val (fixdef_thms, thy') =
- PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
+ PureThy.add_defs false (map Thm.no_attributes 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));
--- a/src/HOLCF/Tools/pcpodef_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -90,7 +90,7 @@
|> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
(Class.intro_classes_tac [])
- ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
+ ||>> PureThy.add_defs true [Thm.no_attributes less_def]
|-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
(Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
--- a/src/Pure/Isar/constdefs.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/Isar/constdefs.ML Tue Jul 29 08:15:40 2008 +0200
@@ -50,7 +50,7 @@
val thy' =
thy
|> Sign.add_consts_i [(c, T, mx)]
- |> PureThy.add_defs_i false [((name, def), atts)]
+ |> PureThy.add_defs false [((name, def), atts)]
|-> (fn [thm] => Code.add_default_func thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/isar_cmd.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Jul 29 08:15:40 2008 +0200
@@ -192,20 +192,20 @@
fun add_axms f args thy =
f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
-val add_axioms = add_axms (snd oo PureThy.add_axioms);
+val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
fun add_defs ((unchecked, overloaded), args) =
add_axms
- (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args;
+ (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
(* facts *)
fun apply_theorems args thy =
let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)]
- in apfst (maps snd) (PureThy.note_thmss "" facts thy) end;
+ in apfst (maps snd) (PureThy.note_thmss_cmd "" facts thy) end;
-fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)];
+fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss "" [(("", []), args)];
(* declarations *)
--- a/src/Pure/Proof/extraction.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Jul 29 08:15:40 2008 +0200
@@ -729,7 +729,7 @@
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_i false [((extr_name s vs ^ "_def",
+ |> PureThy.add_defs false [((extr_name s vs ^ "_def",
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
thy'
--- a/src/Pure/axclass.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/axclass.ML Tue Jul 29 08:15:40 2008 +0200
@@ -468,7 +468,7 @@
val ([def], def_thy) =
thy
|> Sign.primitive_class (bclass, super)
- |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])];
+ |> PureThy.add_defs false [((Thm.def_name bconst, class_eq), [])];
val (raw_intro, (raw_classrel, raw_axioms)) =
split_defined (length conjs) def ||> chop (length super);
@@ -478,10 +478,13 @@
val class_triv = Thm.class_triv def_thy class;
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
def_thy
- |> PureThy.note_thmss_qualified "" bconst
+ |> Sign.add_path bconst
+ |> Sign.no_base_names
+ |> PureThy.note_thmss ""
[((introN, []), [([Drule.standard raw_intro], [])]),
((superN, []), [(map Drule.standard raw_classrel, [])]),
- ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])];
+ ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
+ ||> Sign.restore_naming def_thy;
(* result *)
@@ -491,7 +494,7 @@
facts_thy
|> fold put_classrel (map (pair class) super ~~ classrel)
|> Sign.add_path bconst
- |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
+ |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
|> Sign.restore_naming facts_thy
|> map_axclasses (fn (axclasses, parameters) =>
(Symtab.update (class, axclass) axclasses,
@@ -510,7 +513,7 @@
val args = prep thy raw_args;
val specs = mk args;
val names = name args;
- in thy |> PureThy.add_axioms_i (map (rpair []) (names ~~ specs)) |-> fold add end;
+ in thy |> PureThy.add_axioms (map (rpair []) (names ~~ specs)) |-> fold add end;
fun ax_classrel prep =
axiomatize (map o prep) (map Logic.mk_classrel)
--- a/src/Pure/pure_thy.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/Pure/pure_thy.ML Tue Jul 29 08:15:40 2008 +0200
@@ -43,27 +43,25 @@
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_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * 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 -> ((bstring * attribute list) *
- (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
- val note_thmss_i: string -> ((bstring * attribute list) *
(thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
(thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
- val note_thmss_qualified: string -> string -> ((bstring * attribute list) *
- (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
- val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
- val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
- val add_defs: bool -> ((bstring * string) * attribute list) list ->
+ val note_thmss_cmd: string -> ((bstring * attribute list) *
+ (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
+ val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
+ val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
+ val add_defs: bool -> ((bstring * term) * attribute list) list ->
theory -> thm list * theory
- val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
+ val add_defs_unchecked: bool -> ((bstring * term) * attribute list) list ->
theory -> thm list * theory
- val add_defs_unchecked: bool -> ((bstring * string) * attribute list) list ->
+ val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
theory -> thm list * theory
- val add_defs_unchecked_i: bool -> ((bstring * term) * attribute list) list ->
+ 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
@@ -252,19 +250,12 @@
in
-fun note_thmss k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
-fun note_thmss_i k = gen_note_thmss (K I) (kind k);
+fun note_thmss k = gen_note_thmss (K I) (kind k);
fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g);
+fun note_thmss_cmd k = gen_note_thmss (fn thy => get_fact (Context.Theory thy) thy) (kind k);
end;
-fun note_thmss_qualified k path facts thy =
- thy
- |> Sign.add_path path
- |> Sign.no_base_names
- |> note_thmss_i k facts
- ||> Sign.restore_naming thy;
-
(* store axioms as theorems *)
@@ -278,12 +269,12 @@
val thm = hd (get_axs thy' named_ax);
in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
in
- val add_axioms = add_axm Theory.add_axioms;
- val add_axioms_i = add_axm Theory.add_axioms_i;
- val add_defs = add_axm o Theory.add_defs false;
- val add_defs_i = add_axm o Theory.add_defs_i false;
- val add_defs_unchecked = add_axm o Theory.add_defs true;
- val add_defs_unchecked_i = add_axm o Theory.add_defs_i true;
+ 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;
end;
@@ -414,7 +405,7 @@
#> Sign.add_consts_i
[("term", typ "'a => prop", NoSyn),
("conjunction", typ "prop => prop => prop", NoSyn)]
- #> (add_defs_i false o map Thm.no_attributes)
+ #> (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)"),
("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
--- a/src/ZF/Tools/datatype_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -247,14 +247,14 @@
if need_recursor then
thy |> Sign.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> (snd o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
+ |> (snd o PureThy.add_defs false [Thm.no_attributes recursor_def])
else thy;
val (con_defs, thy0) = thy_path
|> Sign.add_consts_i
((case_base_name, case_typ, NoSyn) ::
map #1 (List.concat con_ty_lists))
- |> PureThy.add_defs_i false
+ |> PureThy.add_defs false
(map Thm.no_attributes
(case_def ::
List.concat (ListPair.map mk_con_defs
--- a/src/ZF/Tools/ind_cases.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/ind_cases.ML Tue Jul 29 08:15:40 2008 +0200
@@ -52,7 +52,7 @@
val facts = args |> map (fn ((name, srcs), props) =>
((name, map (Attrib.attribute thy) srcs),
map (Thm.no_attributes o single o mk_cases) props));
- in thy |> PureThy.note_thmss_i "" facts |> snd end;
+ in thy |> PureThy.note_thmss "" facts |> snd end;
(* ind_cases method *)
--- a/src/ZF/Tools/inductive_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -174,7 +174,7 @@
val (_, thy1) =
thy
|> Sign.add_path big_rec_base_name
- |> PureThy.add_defs_i false (map Thm.no_attributes axpairs);
+ |> PureThy.add_defs false (map Thm.no_attributes axpairs);
val ctxt1 = ProofContext.init thy1;
--- a/src/ZF/Tools/primrec_package.ML Tue Jul 29 08:15:39 2008 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Jul 29 08:15:40 2008 +0200
@@ -170,7 +170,7 @@
val ([def_thm], thy1) = thy
|> Sign.add_path (Sign.base_name fname)
- |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
+ |> (PureThy.add_defs false o map Thm.no_attributes) [def];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val eqn_thms =