src/HOL/Tools/record_package.ML
changeset 6519 5bd1c469e742
parent 6394 3d9fd50fcc43
child 6556 daa00919502b
     1.1 --- a/src/HOL/Tools/record_package.ML	Tue Apr 27 10:47:40 1999 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Apr 27 10:49:52 1999 +0200
     1.3 @@ -29,9 +29,9 @@
     1.4    val mk_update: term -> string * term -> term
     1.5    val print_records: theory -> unit
     1.6    val add_record: (string list * bstring) -> string option
     1.7 -    -> (bstring * string) list -> theory -> theory
     1.8 +    -> (bstring * string) list -> theory -> theory * {simps: thm list, iffs: thm list}
     1.9    val add_record_i: (string list * bstring) -> (typ list * string) option
    1.10 -    -> (bstring * typ) list -> theory -> theory
    1.11 +    -> (bstring * typ) list -> theory -> theory * {simps: thm list, iffs: thm list}
    1.12    val setup: (theory -> theory) list
    1.13  end;
    1.14  
    1.15 @@ -47,14 +47,7 @@
    1.16  fun message s = if ! quiet_mode then () else writeln s;
    1.17  
    1.18  
    1.19 -(* attributes etc. *)        (* FIXME move to Provers *)
    1.20 -
    1.21 -fun add_iffs_global (thy, th) =
    1.22 -  let
    1.23 -    val ss = Simplifier.simpset_ref_of thy;
    1.24 -    val cs = Classical.claset_ref_of thy;
    1.25 -    val (cs', ss') = (! cs, ! ss) addIffs [th];
    1.26 -  in ss := ss'; cs := cs'; (thy, th) end;
    1.27 +(* wrappers *)
    1.28  
    1.29  fun add_wrapper wrapper thy =
    1.30    let val r = Classical.claset_ref_of thy
    1.31 @@ -732,6 +725,7 @@
    1.32      val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props;
    1.33  
    1.34      val simps = field_simps @ sel_convs @ update_convs @ make_defs;
    1.35 +    val iffs = field_injects;
    1.36  
    1.37      val thms_thy =
    1.38        defs_thy
    1.39 @@ -743,7 +737,7 @@
    1.40            ("update_convs", update_convs)]
    1.41        |> PureThy.add_thmss
    1.42          [(("simps", simps), [Simplifier.simp_add_global]),
    1.43 -         (("iffs", field_injects), [add_iffs_global])];
    1.44 +         (("iffs", iffs), [iff_add_global])];
    1.45  
    1.46  
    1.47      (* 4th stage: final_thy *)
    1.48 @@ -754,7 +748,7 @@
    1.49        |> add_record_splits named_splits
    1.50        |> Theory.parent_path;
    1.51  
    1.52 -  in final_thy end;
    1.53 +  in (final_thy, {simps = simps, iffs = iffs}) end;
    1.54  
    1.55  
    1.56  
    1.57 @@ -891,7 +885,7 @@
    1.58  
    1.59  val recordP =
    1.60    OuterSyntax.command "record" "define extensible record"
    1.61 -    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
    1.62 +    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (#1 o add_record x y z)));
    1.63  
    1.64  val _ = OuterSyntax.add_parsers [recordP];
    1.65