# HG changeset patch # User haftmann # Date 1217312140 -7200 # Node ID ce171cbd4b93466346a2d77997b36afd3cfa1b5e # Parent 24738db98d34963d852864230bb8810c778099a8 PureThy: dropped note_thmss_qualified, dropped _i suffix diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Import/proof_kernel.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Import/replay.ML --- 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 = diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Nominal/nominal_atoms.ML --- 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 *) diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Nominal/nominal_package.ML --- 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')))))) diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Nominal/nominal_primrec.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Statespace/DistinctTreeProver.thy --- 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) *} diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/TFL/tfl.ML --- 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) diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/datatype_abs_proofs.ML --- 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 ~~ diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/datatype_rep_proofs.ML --- 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 *) diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/function_package/size.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/old_primrec_package.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/record_package.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/specification_package.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/typedef_package.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/IOA/meta_theory/ioa_package.ML --- 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) diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/Tools/domain/domain_axioms.ML --- 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 *) diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/Tools/fixrec_package.ML --- 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)); diff -r 24738db98d34 -r ce171cbd4b93 src/HOLCF/Tools/pcpodef_package.ML --- 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) diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/Isar/constdefs.ML --- 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; diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/Isar/isar_cmd.ML --- 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 *) diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/Proof/extraction.ML --- 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' diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/axclass.ML --- 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) diff -r 24738db98d34 -r ce171cbd4b93 src/Pure/pure_thy.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/datatype_package.ML --- 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 diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/ind_cases.ML --- 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 *) diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/inductive_package.ML --- 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; diff -r 24738db98d34 -r ce171cbd4b93 src/ZF/Tools/primrec_package.ML --- 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 =