# HG changeset patch # User wenzelm # Date 925202992 -7200 # Node ID 5bd1c469e742dccb2c1db5b4dc2b5eccf38f8fd4 # Parent e9d6f165f9c102d257cd4c75ff6b8b4e1929b2b7 iff_add_global (from simpdata.ML); diff -r e9d6f165f9c1 -r 5bd1c469e742 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Apr 27 10:47:40 1999 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Apr 27 10:49:52 1999 +0200 @@ -29,9 +29,9 @@ val mk_update: term -> string * term -> term val print_records: theory -> unit val add_record: (string list * bstring) -> string option - -> (bstring * string) list -> theory -> theory + -> (bstring * string) list -> theory -> theory * {simps: thm list, iffs: thm list} val add_record_i: (string list * bstring) -> (typ list * string) option - -> (bstring * typ) list -> theory -> theory + -> (bstring * typ) list -> theory -> theory * {simps: thm list, iffs: thm list} val setup: (theory -> theory) list end; @@ -47,14 +47,7 @@ fun message s = if ! quiet_mode then () else writeln s; -(* attributes etc. *) (* FIXME move to Provers *) - -fun add_iffs_global (thy, th) = - let - val ss = Simplifier.simpset_ref_of thy; - val cs = Classical.claset_ref_of thy; - val (cs', ss') = (! cs, ! ss) addIffs [th]; - in ss := ss'; cs := cs'; (thy, th) end; +(* wrappers *) fun add_wrapper wrapper thy = let val r = Classical.claset_ref_of thy @@ -732,6 +725,7 @@ val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props; val simps = field_simps @ sel_convs @ update_convs @ make_defs; + val iffs = field_injects; val thms_thy = defs_thy @@ -743,7 +737,7 @@ ("update_convs", update_convs)] |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global]), - (("iffs", field_injects), [add_iffs_global])]; + (("iffs", iffs), [iff_add_global])]; (* 4th stage: final_thy *) @@ -754,7 +748,7 @@ |> add_record_splits named_splits |> Theory.parent_path; - in final_thy end; + in (final_thy, {simps = simps, iffs = iffs}) end; @@ -891,7 +885,7 @@ val recordP = OuterSyntax.command "record" "define extensible record" - (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); + (record_decl >> (fn (x, (y, z)) => Toplevel.theory (#1 o add_record x y z))); val _ = OuterSyntax.add_parsers [recordP];