# HG changeset patch # User wenzelm # Date 963522790 -7200 # Node ID f793f05024f6f2718ba2a259e8a0b7a315ab5e09 # Parent fd8b0f2198796983146d8e9cc16736fa3245950e adapted PureThy.add_defs_i; diff -r fd8b0f219879 -r f793f05024f6 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Jul 13 23:13:10 2000 +0200 @@ -262,7 +262,7 @@ Theory.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 o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => + (PureThy.add_defs_i 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 ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))) @@ -344,7 +344,7 @@ list_comb (reccomb, (flat (take (i, case_dummy_fns))) @ fns2 @ (flat (drop (i + 1, case_dummy_fns))) ))); val (thy', [def_thm]) = thy |> - Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def]; + Theory.add_consts_i [decl] |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy') end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ @@ -446,7 +446,7 @@ Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T --> HOLogic.natT, NoSyn)) (drop (length (hd descr), size_names ~~ recTs))) |> - (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) => + (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) => (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))) (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>> diff -r fd8b0f219879 -r f793f05024f6 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Jul 13 23:13:10 2000 +0200 @@ -233,7 +233,7 @@ (Const (rep_name, T --> Univ_elT) $ lhs, rhs)); val (thy', [def_thm]) = thy |> Theory.add_consts_i [(cname', constrT, mx)] |> - (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)]; + (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; @@ -381,7 +381,7 @@ val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $ list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos); - val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy; + val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; (* prove characteristic equations *) diff -r fd8b0f219879 -r f793f05024f6 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/inductive_package.ML Thu Jul 13 23:13:10 2000 +0200 @@ -653,7 +653,7 @@ |> (if length cs < 2 then I else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |> Theory.add_path rec_name - |> PureThy.add_defss_i [(("defs", def_terms), [])]; + |> PureThy.add_defss_i false [(("defs", def_terms), [])]; val mono = prove_mono setT fp_fun monos thy' diff -r fd8b0f219879 -r f793f05024f6 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/primrec_package.ML Thu Jul 13 23:13:10 2000 +0200 @@ -296,7 +296,7 @@ val primrec_name = if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name; val (thy', defs_thms') = thy |> Theory.add_path primrec_name |> - (if eq_set (names1, names2) then (PureThy.add_defs_i o map Thm.no_attributes) defs' + (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs' else primrec_err ("functions " ^ commas_quote names2 ^ "\nare not mutually recursive")); val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms'; diff -r fd8b0f219879 -r f793f05024f6 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Jul 13 23:13:10 2000 +0200 @@ -619,8 +619,8 @@ val (defs_thy, (field_defs, dest_defs)) = 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, [Drule.tag_internal]))) field_specs - |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) dest_specs; + |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) field_specs + |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) dest_specs; (* 3rd stage: thms_thy *) @@ -789,9 +789,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, [Drule.tag_internal]))) sel_specs - |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) update_specs - |>>> (PureThy.add_defs_i o map Thm.no_attributes) make_specs; + |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) sel_specs + |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) update_specs + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs; (* 3rd stage: thms_thy *) diff -r fd8b0f219879 -r f793f05024f6 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/typedef_package.ML Thu Jul 13 23:13:10 2000 +0200 @@ -141,7 +141,7 @@ ((if no_def then [] else [(name, setT, NoSyn)]) @ [(Rep_name, newT --> oldT, NoSyn), (Abs_name, oldT --> newT, NoSyn)]) - |> (if no_def then I else (#1 oo (PureThy.add_defs_i o map Thm.no_attributes)) + |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes)) [Logic.mk_defpair (setC, set)]) |> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes)) [(Rep_name, rep_type),